mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Subsemigroup.Defs
MulMemClass.mk_mul_mk : ∀ {M : Type u_1} {A : Type u_3} [inst : Mul M] [inst_1 : SetLike A M] [hA : MulMemClass A M] (S' : A) (x y : M)
  (hx : x ∈ S') (hy : y ∈ S'), ⟨x, hx⟩ * ⟨y, hy⟩ = ⟨x * y, ⋯⟩
-- Mathlib.CategoryTheory.Limits.ConeCategory
CategoryTheory.Limits.Cone.toStructuredArrow_obj : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F) (j : J),
  c.toStructuredArrow.obj j = CategoryTheory.StructuredArrow.mk (c.π.app j)
-- Std.Async.System
Std.Async.System.GroupId.mk.injEq : ∀ (toNat toNat_1 : ℕ), ({ toNat := toNat } = { toNat := toNat_1 }) = (toNat = toNat_1)
-- Mathlib.Algebra.Colimit.Module
Module.DirectLimit.lift_comp_of : ∀ {R : Type u_1} [inst : Semiring R] {ι : Type u_2} [inst_1 : Preorder ι] {G : ι → Type u_3}
  [inst_2 : (i : ι) → AddCommMonoid (G i)] [inst_3 : (i : ι) → Module R (G i)] {f : (i j : ι) → i ≤ j → G i →ₗ[R] G j}
  [inst_4 : DecidableEq ι] {P : Type u_4} [inst_5 : AddCommMonoid P] [inst_6 : Module R P]
  (F : Module.DirectLimit G f →ₗ[R] P),
  Module.DirectLimit.lift R ι G f (fun i => F ∘ₗ Module.DirectLimit.of R ι G f i) ⋯ = F
-- Init.Data.Int.Gcd
Int.gcd_one_left : ∀ (a : ℤ), Int.gcd 1 a = 1
-- Mathlib.Algebra.BigOperators.Intervals
Finset.sum_range_succ_sub_sum : ∀ {M : Type u_4} (f : ℕ → M) {n : ℕ} [inst : AddCommGroup M],
  ∑ i ∈ Finset.range (n + 1), f i - ∑ i ∈ Finset.range n, f i = f n
-- Std.Data.DHashMap.Internal.RawLemmas
_private.Std.Data.DHashMap.Internal.RawLemmas.0.Std.DHashMap.Internal.Raw₀.get!.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] [inst_2 : Hashable α] (a : α)
  [inst_3 : Inhabited (β a)] (size : ℕ) (buckets : Array (Std.DHashMap.Internal.AssocList α β))
  (hm : 0 < { size := size, buckets := buckets }.buckets.size),
  Std.DHashMap.Internal.Raw₀.get! ⟨{ size := size, buckets := buckets }, hm⟩ a =
    Std.DHashMap.Internal.AssocList.getCast! a buckets[↑(Std.DHashMap.Internal.mkIdx buckets.size hm (hash a))]
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.closure_closure_coe_preimage : ∀ {M : Type u_5} [inst : AddZeroClass M] {s : Set M}, AddSubmonoid.closure (Subtype.val ⁻¹' s) = ⊤
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.biproduct.π_epi : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] (f : J → C) [inst_2 : CategoryTheory.Limits.HasBiproduct f]
  (b : J), CategoryTheory.IsSplitEpi (CategoryTheory.Limits.biproduct.π f b)
-- Mathlib.Topology.Order.LeftRightLim
Antitone.leftLim : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : ConditionallyCompleteLinearOrder β]
  [inst_2 : TopologicalSpace β] [OrderTopology β] {f : α → β}, Antitone f → Antitone (Function.leftLim f)
-- Init.Prelude
instInhabitedForallOfMonad : {α : Type u} → {m : Type u → Type v} → [Monad m] → Inhabited (α → m α)
-- Init.MetaTypes
/-- When `true` (default: `false`), unfolds applications of functions defined by pattern matching, when one of the patterns applies.
This can be enabled using the `simp!` syntax.
 -/
Lean.Meta.Simp.Config.autoUnfold : Lean.Meta.Simp.Config → Bool
-- Mathlib.RingTheory.WittVector.WittPolynomial
wittPolynomial_one : ∀ (p : ℕ) (R : Type u_1) [inst : CommRing R],
  wittPolynomial p R 1 = MvPolynomial.C ↑p * MvPolynomial.X 1 + MvPolynomial.X 0 ^ p
-- Lean.Environment
Lean.Kernel.Exception.declHasFVars.injEq : ∀ (env : Lean.Kernel.Environment) (name : Lean.Name) (expr : Lean.Expr) (env_1 : Lean.Kernel.Environment)
  (name_1 : Lean.Name) (expr_1 : Lean.Expr),
  (Lean.Kernel.Exception.declHasFVars env name expr = Lean.Kernel.Exception.declHasFVars env_1 name_1 expr_1) =
    (env = env_1 ∧ name = name_1 ∧ expr = expr_1)
-- Init.Prelude
/-- The implementation of `a >> b : α`. See `HAndThen`.  -/
AndThen.andThen : {α : Type u} → [self : AndThen α] → α → (Unit → α) → α
-- Mathlib.Data.Set.Function
Set.LeftInvOn.eqOn : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} {f' : β → α}, Set.LeftInvOn f' f s → Set.EqOn (f' ∘ f) id s
-- Mathlib.Data.Bool.Basic
Decidable.decide.hcongr_2 : ∀ (p p' : Prop), p = p' → ∀ (h : Decidable p) (h' : Decidable p'), h ≍ h' → decide p ≍ decide p'
-- Mathlib.Algebra.GCDMonoid.Basic
lcm_one_left : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] (a : α), lcm 1 a = normalize a
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.Hom.ext_iff : ∀ {k : Type u} {G : Type v} {inst : Semiring k} {inst_1 : Monoid G} {A B : Rep.{w, u, v} k G} {x y : A.Hom B},
  x = y ↔ x.hom' = y.hom'
-- Mathlib.Topology.Category.Profinite.Basic
instFaithfulFintypeCatProfiniteToProfinite : FintypeCat.toProfinite.Faithful
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.minKeyD_insertIfNew_le_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β} {fallback : α}, (cmp ((t.insertIfNew k v).minKeyD fallback) k).isLE = true
-- Mathlib.MeasureTheory.Integral.Lebesgue.Norm
MeasureTheory.lintegral_ofReal_le_lintegral_enorm : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} (f : α → ℝ),
  ∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ ≤ ∫⁻ (x : α), ‖f x‖ₑ ∂μ
-- Batteries.Recycling.RBTree.Basic
_private.Batteries.Recycling.RBTree.Basic.0.RBTree.RBNode.append.match_1.eq_1 : ∀ {α : Type u_1} (motive : RBTree.RBNode α → RBTree.RBNode α → Sort u_2) (x : 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.nil, x 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_1 x
-- Init.Data.Slice.List.Lemmas
_private.Init.Data.Slice.List.Lemmas.0.ListSlice.internalIter_eq : ∀ {α : Type u} {s : ListSlice α},
  Std.Slice.Internal.iter s =
    match s.internalRepresentation.stop with
    | some stop => Std.Iter.take stop s.internalRepresentation.list.iter
    | none => s.internalRepresentation.list.iter.toTake
-- Lean.Elab.MutualDef
Lean.Elab.Term.MutualClosure.ClosureState.mk.injEq : ∀ (newLocalDecls localDecls newLetDecls : Array Lean.LocalDecl) (exprArgs : Array Lean.Expr)
  (newLocalDecls_1 localDecls_1 newLetDecls_1 : Array Lean.LocalDecl) (exprArgs_1 : Array Lean.Expr),
  ({ newLocalDecls := newLocalDecls, localDecls := localDecls, newLetDecls := newLetDecls, exprArgs := exprArgs } =
      { newLocalDecls := newLocalDecls_1, localDecls := localDecls_1, newLetDecls := newLetDecls_1,
        exprArgs := exprArgs_1 }) =
    (newLocalDecls = newLocalDecls_1 ∧ localDecls = localDecls_1 ∧ newLetDecls = newLetDecls_1 ∧ exprArgs = exprArgs_1)
-- Mathlib.CategoryTheory.Abelian.Preradical.Colon
CategoryTheory.Abelian.Preradical.isPullback_colon_obj : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (Φ Ψ : CategoryTheory.Abelian.Preradical C) (X : C),
  CategoryTheory.IsPullback ((Φ.colon Ψ).ι.app X) ((Φ.colonπ Ψ).app X) (Φ.π.app X) (Ψ.ι.app (Φ.quotient.obj X))
-- Mathlib.GroupTheory.IsPerfect
Group.IsPerfect.instQuotientSubgroup : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} [inst_1 : H.Normal] [Group.IsPerfect G], Group.IsPerfect (G ⧸ H)
-- Init.Data.List.Basic
List.map_eq_mapTR : @List.map = @List.mapTR
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
MeasureTheory.condExp_bot : ∀ {α : Type u_1} {E : Type u_3} {m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [CompleteSpace E] [MeasureTheory.IsProbabilityMeasure μ] (f : α → E),
  μ[f | ⊥] = fun x => ∫ (x : α), f x ∂μ
-- Lean.DocString.Formatter
_private.Lean.DocString.Formatter.0.Lean.Doc.Parser.rep : Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter
-- Mathlib.CategoryTheory.Abelian.SerreClass.Localization
CategoryTheory.ObjectProperty.SerreClassLocalization.hasCoequalizers : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {D : Type u'}
  [inst_2 : CategoryTheory.Category.{v', u'} D] (L : CategoryTheory.Functor C D) (P : CategoryTheory.ObjectProperty C)
  [inst_3 : P.IsSerreClass] [L.IsLocalization P.isoModSerre] [inst_5 : CategoryTheory.Preadditive D] [L.Additive],
  CategoryTheory.Limits.HasCoequalizers D
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
/-- Evaluate the expression `α ≫ η` into a normalized form.  -/
Mathlib.Tactic.BicategoryLike.evalCompNil : {ρ : Type} →
  [Mathlib.Tactic.BicategoryLike.MonadMor₂Iso (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] →
    [Mathlib.Tactic.BicategoryLike.MonadNormalExpr (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] →
      [Mathlib.Tactic.BicategoryLike.MkEval (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] →
        Mathlib.Tactic.BicategoryLike.Structural →
          Mathlib.Tactic.BicategoryLike.NormalExpr →
            Mathlib.Tactic.BicategoryLike.CoherenceM ρ Mathlib.Tactic.BicategoryLike.Eval.Result
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackContinuous
/-- The pullback of (pre)sheaves of modules commutes with the sheafification.  -/
SheafOfModules.sheafificationCompPullback : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {J : CategoryTheory.GrothendieckTopology C} →
          {K : CategoryTheory.GrothendieckTopology D} →
            {F : CategoryTheory.Functor C D} →
              {S : CategoryTheory.Sheaf J RingCat} →
                {R : CategoryTheory.Sheaf K RingCat} →
                  [inst_2 : F.IsContinuous J K] →
                    (φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R) →
                      [inst_3 : (PresheafOfModules.pushforward φ.hom).IsRightAdjoint] →
                        [inst_4 : CategoryTheory.HasWeakSheafify K AddCommGrpCat] →
                          [inst_5 : K.WEqualsLocallyBijective AddCommGrpCat] →
                            [inst_6 : CategoryTheory.HasWeakSheafify J AddCommGrpCat] →
                              [inst_7 : J.WEqualsLocallyBijective AddCommGrpCat] →
                                (PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id S.obj)).comp
                                    (SheafOfModules.pullback φ) ≅
                                  (PresheafOfModules.pullback φ.hom).comp
                                    (PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id R.obj))
-- Mathlib.Analysis.Asymptotics.TVS
Asymptotics.IsLittleOTVS.insert : ∀ {α : 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] {f : α → E} {g : α → F} [inst_7 : TopologicalSpace α] {x : α}
  {s : Set α}, f =o[𝕜; nhdsWithin x s] g → f x = 0 → f =o[𝕜; nhdsWithin x (insert x s)] g
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Equiv.keys_perm : ∀ {α : Type u} {β : α → Type v} {m₁ m₂ : Std.DHashMap.Raw α β}, m₁.Equiv m₂ → m₁.keys.Perm m₂.keys
-- Mathlib.RingTheory.Extension.Generators
/-- Given two families of generators `S[X] → T` and `R[Y] → S`,
we may construct the family of generators `R[X, Y] → T`.  -/
Algebra.Generators.comp : {R : Type u} →
  {S : Type v} →
    {ι : Type w} →
      [inst : CommRing R] →
        [inst_1 : CommRing S] →
          [inst_2 : Algebra R S] →
            {ι' : Type u_1} →
              {T : Type u_2} →
                [inst_3 : CommRing T] →
                  [inst_4 : Algebra R T] →
                    [inst_5 : Algebra S T] →
                      [IsScalarTower R S T] →
                        Algebra.Generators S T ι' → Algebra.Generators R S ι → Algebra.Generators R T (ι' ⊕ ι)
-- Mathlib.MeasureTheory.Group.Measure
/-- In an abelian additive group every left invariant measure is also right-invariant. We don't
declare the converse as an instance, since that would loop type-class inference, and we use
`IsAddLeftInvariant` as the default hypothesis in abelian groups.  -/
MeasureTheory.IsAddLeftInvariant.isAddRightInvariant : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : AddCommSemigroup G] {μ : MeasureTheory.Measure G}
  [μ.IsAddLeftInvariant], μ.IsAddRightInvariant
-- Mathlib.CategoryTheory.Bicategory.CatEnriched
CategoryTheory.CatEnrichedOrdinary.id_eq_eqToHom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (X : C),
  CategoryTheory.CategoryStruct.id X = CategoryTheory.eqToHom ⋯
-- Lean.AddDecl
/-- Adds the given declaration to the environment's private scope, deriving a suitable presentation in
the public scope if under the module system and if the declaration is not private. If `forceExpose`
is true, exposes the declaration body, i.e. preserves the full representation in the public scope,
independently of `Environment.isExporting` and even for theorems.
 -/
Lean.addDecl : Lean.Declaration → optParam Bool false → Lean.CoreM Unit
-- Init.Prelude
Max.mk : {α : Type u} → (α → α → α) → Max α
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.cyclesMap_comp_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} {K L M : HomologicalComplex C c} (φ : K ⟶ L) (ψ : L ⟶ M) (i : ι)
  [inst_2 : K.HasHomology i] [inst_3 : L.HasHomology i] [inst_4 : M.HasHomology i] {Z : C} (h : M.cycles i ⟶ Z),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.cyclesMap (CategoryTheory.CategoryStruct.comp φ ψ) i) h =
    CategoryTheory.CategoryStruct.comp (HomologicalComplex.cyclesMap φ i)
      (CategoryTheory.CategoryStruct.comp (HomologicalComplex.cyclesMap ψ i) h)
-- Mathlib.CategoryTheory.Monoidal.Comon_
CategoryTheory.Comon.trivial_comon_comul : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C],
  CategoryTheory.ComonObj.comul =
    (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv
-- Mathlib.Analysis.Calculus.FDeriv.Mul
HasStrictFDerivAt.list_prod' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {ι : Type u_5} {𝔸 : Type u_6} [inst_3 : NormedRing 𝔸] [inst_4 : NormedAlgebra 𝕜 𝔸]
  {f : ι → E → 𝔸} {f' : ι → E →L[𝕜] 𝔸} {l : List ι} {x : E},
  (∀ i ∈ l, HasStrictFDerivAt (fun x => f i x) (f' i) x) →
    HasStrictFDerivAt (fun x => (List.map (fun x_1 => f x_1 x) l).prod)
      (∑ i,
        (List.map (fun x_1 => f x_1 x) (List.take (↑i) l)).prod •
          MulOpposite.op (List.map (fun x_1 => f x_1 x) (List.drop (↑i).succ l)).prod • f' l[i])
      x
-- Mathlib.Data.Sum.Interval
Sum.Ioc_inl_inl : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : LocallyFiniteOrder α]
  [inst_3 : LocallyFiniteOrder β] (a₁ a₂ : α),
  Finset.Ioc (Sum.inl a₁) (Sum.inl a₂) = Finset.map Function.Embedding.inl (Finset.Ioc a₁ a₂)
-- Mathlib.Algebra.Notation.Indicator
Set.mulIndicator_const_preimage_eq_union : ∀ {α : Type u_1} {M : Type u_3} [inst : One M] (U : Set α) (s : Set M) (a : M) [inst_1 : Decidable (a ∈ s)]
  [inst_2 : Decidable (1 ∈ s)], (U.mulIndicator fun x => a) ⁻¹' s = (if a ∈ s then U else ∅) ∪ if 1 ∈ s then Uᶜ else ∅
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
CategoryTheory.Bicategory.adjointifyCounit_left_triangle : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {a b : B} {f : a ⟶ b} {g : b ⟶ a}
  (η : CategoryTheory.CategoryStruct.id a ≅ CategoryTheory.CategoryStruct.comp f g)
  (ε : CategoryTheory.CategoryStruct.comp g f ≅ CategoryTheory.CategoryStruct.id b),
  CategoryTheory.Bicategory.leftZigzagIso η (CategoryTheory.Bicategory.adjointifyCounit η ε) =
    CategoryTheory.Bicategory.leftUnitor f ≪≫ (CategoryTheory.Bicategory.rightUnitor f).symm
-- Mathlib.Topology.Algebra.Group.Basic
/-- The topological closure of a normal additive subgroup is normal.  -/
AddSubgroup.is_normal_topologicalClosure : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [inst_2 : IsTopologicalAddGroup G]
  (N : AddSubgroup G) [N.Normal], N.topologicalClosure.Normal
-- Mathlib.CategoryTheory.ObjectProperty.Small
CategoryTheory.ObjectProperty.instEssentiallySmallISupOfSmall : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {α : Type u_1} (P : α → CategoryTheory.ObjectProperty C)
  [∀ (a : α), CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} (P a)] [Small.{w, u_1} α],
  CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} (⨆ a, P a)
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instSub : {α : Type u_1} → {l : Filter α} → {M : Type u_5} → [Sub M] → Sub (l.Germ M)
-- Std.Http.Data.Status
/-- 305 Use Proxy
 -/
Std.Http.Status.useProxy : Std.Http.Status
-- Mathlib.Algebra.Group.Subsemigroup.Defs
Subsemigroup.instPartialOrder : {M : Type u_1} → [inst : Mul M] → PartialOrder (Subsemigroup M)
-- Mathlib.CategoryTheory.Monad.Basic
CategoryTheory.MonadHom.app_μ : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {T₁ T₂ : CategoryTheory.Monad C}
  (self : CategoryTheory.MonadHom T₁ T₂) (X : C),
  CategoryTheory.CategoryStruct.comp (T₁.μ.app X) (self.app X) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (T₁.map (self.app X)) (self.app (T₂.obj X)))
      (T₂.μ.app X)
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
/-- If `f b = 0`, then the sum of `f a` with `a ∈ s` is the same as the sum of `f a`
for `a ∈ s ∖ {b}`.  -/
tsum_eq_tsum_sdiff_singleton : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α} (s : Set β) {b : β},
  f b = 0 → ∑' (a : ↑s), f ↑a = ∑' (a : ↑(s \ {b})), f ↑a
-- Lean.Parser.Types
Lean.Parser.instInhabitedError : Inhabited Lean.Parser.Error
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
mem_of_mem_measurableAtom : ∀ {β : Type u_2} [inst : MeasurableSpace β] {x y : β},
  y ∈ measurableAtom x → ∀ {s : Set β}, MeasurableSet s → x ∈ s → y ∈ s
-- Mathlib.Tactic.Translate.UnfoldBoundary
/-- Modify `e` so that it has type `expectedType` if the constants in `b` cannot be unfolded.  -/
Mathlib.Tactic.UnfoldBoundary.UnfoldBoundaries.cast : Mathlib.Tactic.UnfoldBoundary.UnfoldBoundaries → Lean.Expr → Lean.Expr → Lean.Name → Lean.MetaM Lean.Expr
-- Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
CategoryTheory.Triangulated.TStructure.eTruncGEIsoGEGE.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) [inst_6 : CategoryTheory.IsTriangulated C] (a b : EInt) (hab : a ≤ b),
  t.eTruncGEIsoGEGE a b hab = t.eTruncGEIsoGEGE a b hab
-- Mathlib.Probability.Kernel.Composition.Prod
ProbabilityTheory.Kernel.prodAssoc_prod : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {δ : Type u_5}
  {mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ} (κ : ProbabilityTheory.Kernel α β)
  [ProbabilityTheory.IsSFiniteKernel κ] (η : ProbabilityTheory.Kernel α γ) [ProbabilityTheory.IsSFiniteKernel η]
  (ξ : ProbabilityTheory.Kernel α δ) [ProbabilityTheory.IsSFiniteKernel ξ],
  ((κ.prod ξ).prod η).map ⇑MeasurableEquiv.prodAssoc = κ.prod (ξ.prod η)
-- Mathlib.Order.UpperLower.CompleteLattice
UpperSet.compl_inf : ∀ {α : Type u_1} [inst : LE α] (s t : UpperSet α), (s ⊓ t).compl = s.compl ⊓ t.compl
-- Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
/-- Images in `GL(2, ℝ)` of finite-index subgroups of `SL(2, ℤ)` are arithmetic.  -/
Subgroup.instIsArithmeticMapSpecialLinearGroupFinOfNatNatIntGeneralLinearGroupRealMapGLOfFiniteIndex : ∀ (Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)) [Γ.FiniteIndex],
  (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ).IsArithmetic
-- Mathlib.CategoryTheory.Bicategory.End
CategoryTheory.whiskerRight_def : ∀ {C : Type u} [inst : CategoryTheory.Bicategory C] (X : C) {x x_1 : X ⟶ X} (η : x ⟶ x_1) (h : X ⟶ X),
  CategoryTheory.MonoidalCategoryStruct.whiskerRight η h = CategoryTheory.Bicategory.whiskerRight η h
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.map_sub : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} [inst : Sub α] [inst_1 : Sub β] (f : α → β),
  (∀ (a₁ a₂ : α), f (a₁ - a₂) = f a₁ - f a₂) → ∀ (M N : Matrix m n α), (M - N).map f = M.map f - N.map f
-- Mathlib.Data.FunLike.Group
/-- A `FunLike` type with `1` and `*` is `MulOneClass` if `β` is a `MulOneClass`.  -/
FunLike.mulOneClass : {F : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : FunLike F α β] →
        [inst_1 : Mul F] →
          [inst_2 : One F] → [inst_3 : MulOneClass β] → [IsOneApply F α β] → [IsMulApply F α β] → MulOneClass F
-- Mathlib.Tactic.Simps.Basic
/-- simplify the right-hand side of generated simp-lemmas using `dsimp, simp`.  -/
Simps.Config.simpRhs : Simps.Config → Bool
-- Lean.Elab.PreDefinition.Structural.FindRecArg
/-- Given the `RecArgInfo`s of all the recursive functions, find the inductive groups to consider.
 -/
Lean.Elab.Structural.inductiveGroups : Array Lean.Elab.Structural.RecArgInfo → Lean.MetaM (Array Lean.Elab.Structural.IndGroupInst)
-- Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
CategoryTheory.Limits.Concrete.widePushout_exists_rep' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type v}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC] {B : C}
  {α : Type v} [Nonempty α] {X : α → C} (f : (j : α) → B ⟶ X j) [inst_4 : CategoryTheory.Limits.HasWidePushout B X f]
  [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.WidePushoutShape.wideSpan B X f)
      (CategoryTheory.forget C)]
  (x : CategoryTheory.ToType (CategoryTheory.Limits.widePushout B X f)),
  ∃ i y, (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.WidePushout.ι f i)) y = x
-- Mathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy
/-- Every map of arrows is left homotopic to itself.  -/
CategoryTheory.Arrow.LeftHomotopy.refl : {V : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    [inst_1 : CategoryTheory.Preadditive V] →
      {u v : CategoryTheory.Arrow V} → (f : u ⟶ v) → CategoryTheory.Arrow.LeftHomotopy f f