mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.closure_prod : ∀ {N : Type u_2} [inst : AddZeroClass N] {M : Type u_5} [inst_1 : AddZeroClass M] {s : Set M} {t : Set N},
  0 ∈ s → 0 ∈ t → AddSubmonoid.closure (s ×ˢ t) = (AddSubmonoid.closure s).prod (AddSubmonoid.closure t)
-- Mathlib.Data.Fintype.EquivFin
/-- Any type is (classically) either a `Fintype`, or `Infinite`.

One can obtain the relevant typeclasses via `cases fintypeOrInfinite α`.
 -/
fintypeOrInfinite : (α : Type u_4) → Fintype α ⊕' Infinite α
-- Mathlib.FieldTheory.Galois.IsGaloisGroup
IsGaloisGroup.restrictHom_surjective : ∀ (G : Type u_1) (G' : Type u_2) [inst : Group G] [inst_1 : Group G'] (A : Type u_5) (B : Type u_6) (C : Type u_7)
  [inst_2 : CommRing A] [inst_3 : CommRing B] [inst_4 : CommRing C] [inst_5 : IsDomain C] [inst_6 : Algebra A B]
  [inst_7 : Algebra A C] [inst_8 : Algebra B C] [inst_9 : FaithfulSMul A B] [inst_10 : FaithfulSMul B C]
  [inst_11 : IsScalarTower A B C] [inst_12 : Finite G] [inst_13 : Finite G'] [inst_14 : MulSemiringAction G C]
  [inst_15 : IsGaloisGroup G A C] [inst_16 : MulSemiringAction G' B] [inst_17 : IsGaloisGroup G' A B],
  Function.Surjective ⇑(IsGaloisGroup.restrictHom G G' A B C)
-- Batteries.Data.BinomialHeap.Basic
Batteries.BinomialHeap.instStream : {α : Type u} → {le : α → α → Bool} → Std.Stream (Batteries.BinomialHeap α le) α
-- Mathlib.NumberTheory.NumberField.Discriminant.Basic
/-- If `|discr K| ≤ N` then the Minkowski bound of `K` is less than `boundOfDiscrBdd`.  -/
NumberField.hermiteTheorem.minkowskiBound_lt_boundOfDiscBdd : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] {N : ℕ},
  |NumberField.discr K| ≤ ↑N →
    NumberField.mixedEmbedding.minkowskiBound K 1 < ↑(NumberField.hermiteTheorem.boundOfDiscBdd N)
-- Mathlib.AlgebraicTopology.SimplicialCategory.Basic
/-- The bijection `(K ⟶ L) ≃ sHom K L _⦋0⦌` for all objects `K` and `L`
in a simplicial category.  -/
CategoryTheory.SimplicialCategory.homEquiv' : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.SimplicialCategory C] →
      (K L : C) → (K ⟶ L) ≃ (CategoryTheory.SimplicialCategory.sHom K L).obj (Opposite.op { len := 0 })
-- Mathlib.Data.Quot
Quotient.out_injective : ∀ {α : Sort u_1} {s : Setoid α}, Function.Injective Quotient.out
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getElem?_diff : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α},
  (t₁ \ t₂)[k]? = if k ∈ t₂ then none else t₁[k]?
-- Mathlib.LinearAlgebra.Matrix.Block
Matrix.det_of_isLowerTriangular : ∀ {m : Type u_3} {R : Type v} [inst : CommRing R] [inst_1 : DecidableEq m] [inst_2 : Fintype m] [inst_3 : LinearOrder m]
  (M : Matrix m m R), M.IsLowerTriangular → M.det = ∏ i, M i i
-- Lean.Elab.Tactic.Omega.Core
/-- Construct the proof term associated to a `bmod` step.  -/
Lean.Elab.Tactic.Omega.Justification.bmodProof : ℕ → ℤ → ℕ → Lean.Omega.Coeffs → Lean.Expr → Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Order.IsNormal
Order.IsNormal.isLUB_image_Iio_of_isSuccLimit : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : LinearOrder β] {f : α → β},
  Order.IsNormal f → ∀ {a : α}, Order.IsSuccLimit a → IsLUB (f '' Set.Iio a) (f a)
-- Init.Data.Vector.DecidableEq
Vector.isEqv_toArray : ∀ {α : Type u_1} {n : ℕ} {r : α → α → Bool} [BEq α] (xs ys : Vector α n), xs.toArray.isEqv ys.toArray r = xs.isEqv ys r
-- Mathlib.Topology.Closure
DenseRange.of_comp : ∀ {X : Type u} [inst : TopologicalSpace X] {α : Type u_1} {β : Type u_2} {f : α → X} {g : β → α},
  DenseRange (f ∘ g) → DenseRange f
-- Lean.LibrarySuggestions.Basic
Lean.LibrarySuggestions.Config : Type
-- Mathlib.Topology.Algebra.Ring.Real
instNoncompactSpaceReal : NoncompactSpace ℝ
-- Mathlib.MeasureTheory.Measure.Haar.Extension
/-- If `φ : A →+ B` and `ψ : B →+ C` define a short exact sequence of additive
topological groups, then we can pull back a continuous compactly supported function `f` on `B` along
`φ` to the continuous compactly supported function `a ↦ f (b + φ a)` on `A`.  -/
TopologicalAddGroup.IsSES.pullback : {A : Type u_1} →
  {B : Type u_2} →
    {C : Type u_3} →
      {E : Type u_4} →
        [inst : AddGroup A] →
          [inst_1 : AddGroup B] →
            [inst_2 : AddGroup C] →
              [inst_3 : TopologicalSpace A] →
                [inst_4 : TopologicalSpace B] →
                  [inst_5 : TopologicalSpace C] →
                    {φ : A →+ B} →
                      {ψ : B →+ C} →
                        TopologicalAddGroup.IsSES φ ψ →
                          [IsTopologicalAddGroup A] →
                            [IsTopologicalAddGroup B] →
                              [inst : NormedAddCommGroup E] →
                                CompactlySupportedContinuousMap B E → B → CompactlySupportedContinuousMap A E
-- Init.Core
DoResultPRBC.return.sizeOf_spec : ∀ {α β σ : Type u} [inst : SizeOf α] [inst_1 : SizeOf β] [inst_2 : SizeOf σ] (a : β) (a_1 : σ),
  sizeOf (DoResultPRBC.return a a_1) = 1 + sizeOf a + sizeOf a_1
-- Mathlib.Algebra.FreeAbelianGroup.Finsupp
FreeAbelianGroup.mem_support_iff : ∀ {X : Type u_1} (x : X) (a : FreeAbelianGroup X), x ∈ a.support ↔ (FreeAbelianGroup.coeff x) a ≠ 0
-- Mathlib.Analysis.Calculus.FDeriv.ContinuousMultilinearMap
DifferentiableOn.continuousMultilinearMapCompContinuousLinearMap : ∀ {𝕜 : Type u_1} {ι : Type u_2} {E : Type u_3} {F : ι → Type u_4} {G : ι → Type u_5} {H : Type u_6}
  [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  [inst_3 : (i : ι) → NormedAddCommGroup (F i)] [inst_4 : (i : ι) → NormedSpace 𝕜 (F i)]
  [inst_5 : (i : ι) → NormedAddCommGroup (G i)] [inst_6 : (i : ι) → NormedSpace 𝕜 (G i)] [inst_7 : NormedAddCommGroup H]
  [inst_8 : NormedSpace 𝕜 H] {f : E → ContinuousMultilinearMap 𝕜 G H} {g : (i : ι) → E → F i →L[𝕜] G i} {s : Set E}
  [Finite ι],
  DifferentiableOn 𝕜 f s →
    (∀ (i : ι), DifferentiableOn 𝕜 (g i) s) →
      DifferentiableOn 𝕜 (fun x => (f x).compContinuousLinearMap fun x_1 => g x_1 x) s
-- Mathlib.Algebra.Group.Basic
eq_iff_eq_of_add_eq_add : ∀ {α : Type u_1} [inst : AddCancelCommMonoid α] {a b c d : α}, a + b = c + d → (a = c ↔ b = d)
-- Lean.Meta.Tactic.FunIndInfo
Lean.Meta.FunIndParamKind.param : Lean.Meta.FunIndParamKind
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.isNone_maxKey?_eq_isEmpty : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → t.maxKey?.isNone = t.isEmpty
-- Mathlib.CategoryTheory.Preadditive.FreydCategory.RightFreyd
CategoryTheory.Preadditive.RightFreyd.instAdditiveFunctor : ∀ (V : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} V] [inst_1 : CategoryTheory.Preadditive V]
  [inst_2 : CategoryTheory.Limits.HasZeroObject V], (CategoryTheory.Preadditive.RightFreyd.functor V).Additive
-- Mathlib.Data.Sym.Basic
/-- `replicate n a` is the sym containing only `a` with multiplicity `n`.  -/
Sym.replicate : {α : Type u_1} → (n : ℕ) → α → Sym α n
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
Finsupp.indicator_eq_sum_single : ∀ {α : Type u_1} {M : Type u_8} [inst : AddCommMonoid M] (s : Finset α) (f : α → M),
  (Finsupp.indicator s fun x x_1 => f x) = ∑ x ∈ s, fun₀ | x => f x
-- Mathlib.Algebra.Homology.ShortComplex.Basic
CategoryTheory.ShortComplex.mk : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X₁ X₂ X₃ : C} →
        (f : X₁ ⟶ X₂) →
          (g : X₂ ⟶ X₃) →
            autoParam (CategoryTheory.CategoryStruct.comp f g = 0) CategoryTheory.ShortComplex.zero._autoParam →
              CategoryTheory.ShortComplex C
-- Init.Sym.Lemmas
Lean.Sym.ite_false : ∀ {α : Sort u} (c : Prop) {inst : Decidable c} (a b : α) {ht : ¬c}, (if c then a else b) = b
-- Mathlib.NumberTheory.Chebyshev
/-- Somewhat arbitrary bound which we use to estimate the second term.  -/
_private.Mathlib.NumberTheory.Chebyshev.0.Chebyshev.sqrt_isLittleO : Real.sqrt =o[Filter.atTop] fun x => x / Real.log x ^ 2
-- Mathlib.LinearAlgebra.Span.Defs
Submodule.mem_span : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {x : M}
  {s : Set M}, x ∈ Submodule.span R s ↔ ∀ (p : Submodule R M), s ⊆ ↑p → x ∈ p
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
inv_lt_inv_iff : ∀ {α : Type u} [inst : Group α] [inst_1 : LT α] [MulLeftStrictMono α] {a b : α} [MulRightStrictMono α],
  a⁻¹ < b⁻¹ ↔ b < a
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.glue!.match_1.congr_eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : Std.DTreeMap.Internal.Impl α β → Sort u_3)
  (r : Std.DTreeMap.Internal.Impl α β) (h_1 : Unit → motive Std.DTreeMap.Internal.Impl.leaf)
  (h_2 :
    (r : Std.DTreeMap.Internal.Impl α β) →
      (sz' : ℕ) →
        (k' : α) →
          (v' : β k') →
            (l'' r'' : Std.DTreeMap.Internal.Impl α β) →
              r = Std.DTreeMap.Internal.Impl.inner sz' k' v' l'' r'' →
                motive (Std.DTreeMap.Internal.Impl.inner sz' k' v' l'' r'')),
  r = Std.DTreeMap.Internal.Impl.leaf →
    (match r with
      | Std.DTreeMap.Internal.Impl.leaf => h_1 ()
      | r@h:(Std.DTreeMap.Internal.Impl.inner sz' k' v' l'' r'') => h_2 r sz' k' v' l'' r'' h) ≍
      h_1 ()
-- Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
MvPolynomial.mem_iff_weightedHomogeneousComponent_mem : ∀ (R : Type u_1) {M : Type u_2} [inst : CommSemiring R] {σ : Type u_3} (w : σ → M) [inst_1 : AddCommMonoid M]
  [inst_2 : DecidableEq M] {I : Ideal (MvPolynomial σ R)},
  Ideal.IsHomogeneous (MvPolynomial.weightedHomogeneousSubmodule R w) I →
    ∀ (p : MvPolynomial σ R), p ∈ I ↔ ∀ (m : M), (MvPolynomial.weightedHomogeneousComponent w m) p ∈ I
-- Mathlib.Data.Set.Semiring
SetSemiring.instZero : {α : Type u_1} → Zero (SetSemiring α)
-- Lean.Meta.Match.Basic
Lean.Meta.Match.Alt.mk.sizeOf_spec : ∀ (ref : Lean.Syntax) (idx : ℕ) (rhs : Lean.Expr) (fvarDecls : List Lean.LocalDecl)
  (patterns : List Lean.Meta.Match.Pattern) (cnstrs : List (Lean.Expr × Lean.Expr)) (notAltIdxs : Array ℕ),
  sizeOf
      { ref := ref, idx := idx, rhs := rhs, fvarDecls := fvarDecls, patterns := patterns, cnstrs := cnstrs,
        notAltIdxs := notAltIdxs } =
    1 + sizeOf ref + sizeOf idx + sizeOf rhs + sizeOf fvarDecls + sizeOf patterns + sizeOf cnstrs + sizeOf notAltIdxs
-- Lean.Meta.Canonicalizer
Lean.Meta.Canonicalizer.State.mk.sizeOf_spec : ∀ (cache : Std.HashMap.Raw Lean.Meta.Canonicalizer.ExprVisited UInt64)
  (keyToExprs : Std.HashMap UInt64 (List Lean.Expr)),
  sizeOf { cache := cache, keyToExprs := keyToExprs } = 1 + sizeOf cache + sizeOf keyToExprs
-- Mathlib.Algebra.Ring.Associator
associator_eq_zero_iff_associative : ∀ {R : Type u_1} [inst : NonUnitalNonAssocRing R], associator = 0 ↔ Std.Associative fun x y => x * y
-- Mathlib.Algebra.Lie.Prod
LieHom.inl_injective : ∀ {R : Type u_1} {L₁ : Type u_2} {L₂ : Type u_3} [inst : CommRing R] [inst_1 : LieRing L₁] [inst_2 : LieAlgebra R L₁]
  [inst_3 : LieRing L₂] [inst_4 : LieAlgebra R L₂], Function.Injective ⇑(LieHom.inl R L₁ L₂)
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.isoRestrict_inv_ofRestrict_assoc : ∀ {X Y : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Y) [H : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion f]
  {Z : AlgebraicGeometry.LocallyRingedSpace} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.isoRestrict f).inv
      (CategoryTheory.CategoryStruct.comp f h) =
    CategoryTheory.CategoryStruct.comp (Y.ofRestrict ⋯) h
-- Std.Data.Iterators.Lemmas.Producers.Array
Array.length_iterFromIdx : ∀ {β : Type w} {array : Array β} {pos : ℕ}, (array.iterFromIdx pos).length = array.size - pos
-- Mathlib.Topology.UniformSpace.Cauchy
/-- In a complete uniform space, every Cauchy filter converges.  -/
CompleteSpace.complete : ∀ {α : Type u} {inst : UniformSpace α} [self : CompleteSpace α] {f : Filter α}, Cauchy f → ∃ x, f ≤ nhds x
-- Mathlib.LinearAlgebra.Matrix.RowCol
Matrix.mul_single_eq_updateCol_zero : ∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type v} [inst : DecidableEq m] [inst_1 : DecidableEq n]
  [inst_2 : Fintype m] [inst_3 : NonUnitalNonAssocSemiring α] (A : Matrix l m α) (i : m) (j : n) (r : α),
  A * Matrix.single i j r = Matrix.updateCol 0 j (MulOpposite.op r • A.col i)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.mem_insertManyIfNewUnit_list : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtDHashMap α fun x => Unit} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {l : List α} {k : α},
  k ∈ Std.ExtDHashMap.Const.insertManyIfNewUnit m l ↔ k ∈ m ∨ l.contains k = true
-- Mathlib.CategoryTheory.Presentable.OrthogonalReflection
/-- The projection from `Z` to the multicoequalizer of all morphisms `g₁ g₂ : Y ⟶ step W Z` with
a `f : X ⟶ Y` satisfying `W` such that `f ≫ g₁ = f ≫ g₂`.  -/
CategoryTheory.OrthogonalReflection.fromStep : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (W : CategoryTheory.MorphismProperty C) →
      (Z : C) →
        [inst_1 : CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₁] →
          [inst_2 : CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₂] →
            [inst_3 : CategoryTheory.Limits.HasPushouts C] →
              [inst_4 :
                  CategoryTheory.Limits.HasMulticoequalizer
                    (CategoryTheory.OrthogonalReflection.D₂.multispanIndex W Z)] →
                CategoryTheory.OrthogonalReflection.step W Z ⟶ CategoryTheory.OrthogonalReflection.succ W Z
-- Lean.Expr
/-- Same as `withApp` but with arguments reversed.  -/
Lean.Expr.withAppRev : {α : Sort u_1} → Lean.Expr → (Lean.Expr → Array Lean.Expr → α) → α
-- Mathlib.CategoryTheory.NatIso
CategoryTheory.Iso.hom_inv_id_app_app_assoc : ∀ {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 G : CategoryTheory.Functor C (CategoryTheory.Functor D E)} (e : F ≅ G) (X₁ : C) (X₂ : D) {Z : E}
  (h : (F.obj X₁).obj X₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((e.hom.app X₁).app X₂)
      (CategoryTheory.CategoryStruct.comp ((e.inv.app X₁).app X₂) h) =
    h
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenSubgroup.isClosed : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [SeparatelyContinuousMul G] (U : OpenSubgroup G),
  IsClosed ↑U
-- Mathlib.CategoryTheory.Monoidal.DayConvolution.Closed
CategoryTheory.MonoidalCategory.DayConvolutionInternalHom.mk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {V : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} V] →
        [inst_2 : CategoryTheory.MonoidalCategory C] →
          [inst_3 : CategoryTheory.MonoidalCategory V] →
            [inst_4 : CategoryTheory.MonoidalClosed V] →
              {F G H : CategoryTheory.Functor C V} →
                (π : (c j : C) → H.obj c ⟶ F.obj j ⟹ G.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj j c)) →
                  (hπ :
                      ∀ (c : C) ⦃i j : C⦄ (f : i ⟶ j),
                        CategoryTheory.CategoryStruct.comp (π c i)
                            ((CategoryTheory.ihom (F.obj i)).map
                              (G.map (CategoryTheory.MonoidalCategoryStruct.whiskerRight f c))) =
                          CategoryTheory.CategoryStruct.comp (π c j)
                            ((CategoryTheory.MonoidalClosed.pre (F.map f)).app
                              (G.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj j c)))) →
                    ((c : C) → CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Wedge.mk (H.obj c) (π c) ⋯)) →
                      (∀ {c c' : C} (f : c ⟶ c') (j : C),
                          CategoryTheory.CategoryStruct.comp (H.map f) (π c' j) =
                            CategoryTheory.CategoryStruct.comp (π c j)
                              ((CategoryTheory.ihom (F.obj j)).map
                                (G.map (CategoryTheory.MonoidalCategoryStruct.whiskerLeft j f)))) →
                        CategoryTheory.MonoidalCategory.DayConvolutionInternalHom F G H
-- Init.Data.Nat.Bitwise.Lemmas
Nat.shiftRight_xor_distrib : ∀ {i a b : ℕ}, (a ^^^ b) >>> i = a >>> i ^^^ b >>> i
-- Mathlib.Analysis.SpecialFunctions.Complex.Circle
Circle.periodic_exp : Function.Periodic (⇑Circle.exp) (2 * Real.pi)
-- Mathlib.Algebra.Group.Submonoid.Defs
AddSubmonoid.toAddMonoid.eq_1 : ∀ {M : Type u_5} [inst : AddMonoid M] (S : AddSubmonoid M), S.toAddMonoid = AddSubmonoidClass.toAddMonoid S
-- Mathlib.Algebra.Group.Invertible.Defs
mul_invOf_self' : ∀ {α : Type u} [inst : Mul α] [inst_1 : One α] (a : α) {x : Invertible a}, a * ⅟a = 1
-- Mathlib.Data.Sym.Basic
Sym.decidableMem : {α : Type u_1} → {n : ℕ} → [DecidableEq α] → (a : α) → (s : Sym α n) → Decidable (a ∈ s)
-- Mathlib.Combinatorics.SimpleGraph.Density
Rel.interedges_disjoint_left : ∀ {α : Type u_4} {β : Type u_5} (r : α → β → Prop) [inst : (a : α) → DecidablePred (r a)] {s s' : Finset α},
  Disjoint s s' → ∀ (t : Finset β), Disjoint (Rel.interedges r s t) (Rel.interedges r s' t)
-- Mathlib.CategoryTheory.Monoidal.CommGrp_
CategoryTheory.Functor.mapCommGrp_obj_grp_inv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {D : Type u₂} [inst_3 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_4 : CategoryTheory.CartesianMonoidalCategory D] [inst_5 : CategoryTheory.BraidedCategory D]
  (F : CategoryTheory.Functor C D) [inst_6 : F.Braided] (A : CategoryTheory.CommGrp C),
  CategoryTheory.GrpObj.inv = F.map CategoryTheory.GrpObj.inv
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
ModularGroup.S_mul_S_eq : ↑ModularGroup.S * ↑ModularGroup.S = -1
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
AlgebraicGeometry.LocallyQuasiFinite.of_injective : ∀ {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} [AlgebraicGeometry.LocallyOfFiniteType f],
  Function.Injective ⇑f → AlgebraicGeometry.LocallyQuasiFinite f
-- Mathlib.NumberTheory.LSeries.Nonvanishing
/-- The character we want to show cannot exist.  -/
_private.Mathlib.NumberTheory.LSeries.Nonvanishing.0.DirichletCharacter.BadChar.χ : {N : ℕ} → [inst : NeZero N] → DirichletCharacter.BadChar✝ N → DirichletCharacter ℂ N
-- Mathlib.Combinatorics.Pigeonhole
/-- The pigeonhole principle for finitely many pigeons counted by weight, strict inequality version:
if the total weight of a finite set of pigeons is greater than `n • b`, they are sorted into some
pigeonholes, and for all but `n` pigeonholes the total weight of the pigeons there is nonpositive,
then for at least one of these `n` pigeonholes, the total weight of the pigeons in this pigeonhole
is greater than `b`.  -/
Finset.exists_lt_sum_fiber_of_sum_fiber_nonpos_of_nsmul_lt_sum : ∀ {α : Type u} {β : Type v} {M : Type w} [inst : DecidableEq β] {s : Finset α} {t : Finset β} {f : α → β} {w : α → M}
  {b : M} [inst_1 : AddCommMonoid M] [inst_2 : LinearOrder M] [IsOrderedCancelAddMonoid M],
  (∀ y ∉ t, ∑ x ∈ s with f x = y, w x ≤ 0) → t.card • b < ∑ x ∈ s, w x → ∃ y ∈ t, b < ∑ x ∈ s with f x = y, w x
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.get?_eq_some_iff : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  [inst_2 : LawfulBEq α], (↑m).WF → ∀ {k : α} {v : β k}, m.get? k = some v ↔ ∃ (h : m.contains k = true), m.get k h = v
-- Mathlib.Order.GaloisConnection.Basic
/-- Makes a Galois coinsertion from an order-preserving bijection.  -/
OrderIso.toGaloisCoinsertion : {α : Type u} → {β : Type v} → [inst : Preorder α] → [inst_1 : Preorder β] → (e : α ≃o β) → GaloisCoinsertion ⇑e ⇑e.symm
-- Mathlib.Algebra.GCDMonoid.Multiset
Multiset.lcm_dvd : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] {s : Multiset α} {a : α},
  s.lcm ∣ a ↔ ∀ b ∈ s, b ∣ a
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
/-- Conditional expectation of the indicator of a set, as a linear map from `G` to L1.  -/
MeasureTheory.condExpInd : {α : Type u_1} →
  (G : Type u_4) →
    [inst : NormedAddCommGroup G] →
      [inst_1 : NormedSpace ℝ G] →
        {m m0 : MeasurableSpace α} →
          (hm : m ≤ m0) →
            (μ : MeasureTheory.Measure α) →
              [MeasureTheory.SigmaFinite (μ.trim hm)] → Set α → G →L[ℝ] ↥(MeasureTheory.Lp G 1 μ)
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Pretrivialization.ext'_iff : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  {e e' : Bundle.Pretrivialization F proj}, e = e' ↔ e.toPartialEquiv = e'.toPartialEquiv ∧ e.baseSet = e'.baseSet
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
/-- The Weierstrass `℘` function. This has the notation `℘[L]` in the namespace `PeriodPairs`.  -/
PeriodPair.«term℘'[_]» : Lean.ParserDescr
-- Mathlib.Data.Set.Finite.Lattice
/-- A finite union of finsets is finite.  -/
Set.union_finset_finite_of_range_finite : ∀ {α : Type u} {β : Type v} (f : α → Finset β), (Set.range f).Finite → (⋃ a, ↑(f a)).Finite
-- Batteries.Recycling.RBTree.WF
_private.Batteries.Recycling.RBTree.WF.0.RBTree.RBNode.append.match_1.eq_5 : ∀ {α : Type u_1} (motive : RBTree.RBNode α → RBTree.RBNode α → Sort u_2) (l : RBTree.RBNode α) (v : α)
  (r b : RBTree.RBNode α) (x : α) (c : RBTree.RBNode α) (h_1 : (x : RBTree.RBNode α) → motive RBTree.RBNode.nil x)
  (h_2 : (x : RBTree.RBNode α) → motive x RBTree.RBNode.nil)
  (h_3 :
    (a : RBTree.RBNode α) →
      (x : α) →
        (b c : RBTree.RBNode α) →
          (y : α) →
            (d : RBTree.RBNode α) →
              motive (RBTree.RBNode.node RBTree.RBColor.red a x b) (RBTree.RBNode.node RBTree.RBColor.red c y d))
  (h_4 :
    (a : RBTree.RBNode α) →
      (x : α) →
        (b c : RBTree.RBNode α) →
          (y : α) →
            (d : RBTree.RBNode α) →
              motive (RBTree.RBNode.node RBTree.RBColor.black a x b) (RBTree.RBNode.node RBTree.RBColor.black c y d))
  (h_5 :
    (a l : RBTree.RBNode α) →
      (v : α) →
        (r : RBTree.RBNode α) →
          a = RBTree.RBNode.node RBTree.RBColor.black l v r →
            (b : RBTree.RBNode α) →
              (x : α) →
                (c : RBTree.RBNode α) →
                  motive (RBTree.RBNode.node RBTree.RBColor.black l v r) (RBTree.RBNode.node RBTree.RBColor.red b x c))
  (h_6 :
    (a : RBTree.RBNode α) →
      (x : α) →
        (b c l : RBTree.RBNode α) →
          (v : α) →
            (r : RBTree.RBNode α) →
              c = RBTree.RBNode.node RBTree.RBColor.black l v r →
                motive (RBTree.RBNode.node RBTree.RBColor.red a x b) (RBTree.RBNode.node RBTree.RBColor.black l v r)),
  (match RBTree.RBNode.node RBTree.RBColor.black l v r, RBTree.RBNode.node RBTree.RBColor.red b x c with
    | RBTree.RBNode.nil, x => h_1 x
    | x, RBTree.RBNode.nil => h_2 x
    | RBTree.RBNode.node RBTree.RBColor.red a x b, RBTree.RBNode.node RBTree.RBColor.red c y d => h_3 a x b c y d
    | RBTree.RBNode.node RBTree.RBColor.black a x b, RBTree.RBNode.node RBTree.RBColor.black c y d => h_4 a x b c y d
    | a@h:(RBTree.RBNode.node RBTree.RBColor.black l v r), RBTree.RBNode.node RBTree.RBColor.red b x c =>
      h_5 a l v r h b x c
    | RBTree.RBNode.node RBTree.RBColor.red a x b, c@h:(RBTree.RBNode.node RBTree.RBColor.black l v r) =>
      h_6 a x b c l v r h) =
    h_5 (RBTree.RBNode.node RBTree.RBColor.black l v r) l v r ⋯ b x c
-- Mathlib.GroupTheory.GroupAction.Quotient
/-- **Orbit-stabilizer theorem**.  -/
MulAction.orbitEquivQuotientStabilizer : (G : Type u) →
  {X : Type v} →
    [inst : Group G] → [inst_1 : MulAction G X] → (b : X) → ↑(MulAction.orbit G b) ≃ G ⧸ MulAction.stabilizer G b
-- Init.MetaTypes
Lean.Meta.instInhabitedEtaStructMode : Inhabited Lean.Meta.EtaStructMode
-- Std.Data.DTreeMap.Internal.Zipper
_private.Std.Data.DTreeMap.Internal.Zipper.0.Std.DTreeMap.Internal.RxoIterator.toList_rxoIter : ∀ {α : Type u_1} {β : α → Type u_2} [inst : Ord α] {z : Std.DTreeMap.Internal.Zipper α β} {bound : α},
  { internalState := { iter := z, upper := bound } }.toList =
    List.takeWhile (fun e => (compare e.fst bound).isLT) z.toList