mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Commutator
addCommutatorElement.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G], addCommutatorElement = { bracket := fun g₁ g₂ => g₁ + g₂ + -g₁ + -g₂ }
-- Mathlib.Topology.Algebra.ConstMulAction
IsClosed.smul : ∀ {α : Type u_2} {G : Type u_4} [inst : TopologicalSpace α] [inst_1 : Group G] [inst_2 : MulAction G α]
  [ContinuousConstSMul G α] {s : Set α}, IsClosed s → ∀ (c : G), IsClosed (c • s)
-- Mathlib.Analysis.Fourier.AddCircleMulti
/-- Under the isometric isomorphism `mFourierBasis` from `L²(UnitAddTorus d)` to `ℓ²(ℤᵈ, ℂ)`,
the `i`-th coefficient is `mFourierCoeff f i`.  -/
UnitAddTorus.mFourierBasis_repr : ∀ {d : Type u_1} [inst : Fintype d] (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) (i : d → ℤ),
  ↑(UnitAddTorus.mFourierBasis.repr f) i = UnitAddTorus.mFourierCoeff (↑↑f) i
-- Mathlib.Topology.Category.TopCat.Opens
TopologicalSpace.Opens.mapIso_inv_app : ∀ {X Y : TopCat} (f g : X ⟶ Y) (h : f = g) (U : TopologicalSpace.Opens ↑Y),
  (TopologicalSpace.Opens.mapIso f g h).inv.app U = CategoryTheory.eqToHom ⋯
-- Mathlib.Algebra.Polynomial.Splits
Polynomial.Splits.C_mul_X_pow : ∀ {R : Type u_1} [inst : Semiring R] (a : R) (n : ℕ), (Polynomial.C a * Polynomial.X ^ n).Splits
-- Mathlib.GroupTheory.Perm.Finite
/-- If the permutation `f` maps `{x // p x}` into itself, then this returns the permutation
on `{x // p x}` induced by `f`. Note that the `h` hypothesis is weaker than for
`Equiv.Perm.subtypePerm`.  -/
Equiv.Perm.subtypePermOfFintype : {α : Type u} →
  (f : Equiv.Perm α) → {p : α → Prop} → [Finite { x // p x }] → (∀ (x : α), p x → p (f x)) → Equiv.Perm { x // p x }
-- Mathlib.RingTheory.Idempotents
exists_isIdempotentElem_mul_eq_zero_of_ker_isNilpotent_aux : ∀ {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : Ring S] (f : R →+* S),
  (∀ x ∈ RingHom.ker f, IsNilpotent x) →
    ∀ e₁ ∈ f.range,
      IsIdempotentElem e₁ →
        ∀ (e₂ : R), IsIdempotentElem e₂ → e₁ * f e₂ = 0 → ∃ e', IsIdempotentElem e' ∧ f e' = e₁ ∧ e' * e₂ = 0
-- Std.Http.Internal.Char
Std.Http.Internal.Char.qdtext.eq_4 : ∀ (c : Char),
  (c = '\t' → False) →
    (c = ' ' → False) →
      (c = '!' → False) →
        Std.Http.Internal.Char.qdtext c = (false || decide ('#' ≤ c ∧ c ≤ '[') || decide (']' ≤ c ∧ c ≤ '~'))
-- Mathlib.Data.Set.Card.Arithmetic
Set.exists_union_disjoint_cardinal_eq_iff : ∀ {α : Type u_1} (s : Set α), Even s.ncard ↔ ∃ t u, t ∪ u = s ∧ Disjoint t u ∧ Cardinal.mk ↑t = Cardinal.mk ↑u
-- Std.Data.Internal.List.Associative
Std.Internal.List.containsKey_of_getValueCast?_eq_some : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {l : List ((a : α) × β a)} {a : α} {b : β a},
  Std.Internal.List.getValueCast? a l = some b → Std.Internal.List.containsKey a l = true
-- Mathlib.Order.Disjoint
Codisjoint.ne : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : OrderTop α] {a b : α}, a ≠ ⊤ → Codisjoint a b → a ≠ b
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getD_filter : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} [inst_2 : LawfulBEq α]
  {f : (a : α) → β a → Bool} {k : α} {fallback : β k},
  m.WF → (Std.DHashMap.Raw.filter f m).getD k fallback = (Option.filter (f k) (m.get? k)).getD fallback
-- Mathlib.Algebra.Ring.Parity
natCast_eq_zero_of_even_of_two_eq_zero : ∀ {R : Type u_4} [inst : AddMonoidWithOne R] {n : ℕ}, Even n → 2 = 0 → ↑n = 0
-- Mathlib.Algebra.Group.WithOne.Basic
WithZero.mapAddHom_comp : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Add α] [inst_1 : Add β] [inst_2 : Add γ] (f : α →ₙ+ β) (g : β →ₙ+ γ),
  WithZero.mapAddHom (g.comp f) = (WithZero.mapAddHom g).comp (WithZero.mapAddHom f)
-- Init.Data.Range.Polymorphic.Fin
Fin.least?_eq : ∀ {n : ℕ} [inst : NeZero n], Std.PRange.least? = some 0
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.contains_congr : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k k' : α}, cmp k k' = Ordering.eq → t.contains k = t.contains k'
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Galois
/-- Let `m ∣ n`. Then, the following diagram commutes:
Gal(ℚ(ζₙ)/ℚ) → (ℤ/nℤ)ˣ
  ↓              ↓
Gal(ℚ(ζₘ)/ℚ) → (ℤ/mℤ)ˣ
where the horizontal maps are `galEquivZMod`, the left map is the restriction map and the right map
is the natural map.
 -/
IsCyclotomicExtension.Rat.galEquivZMod_restrictNormal_apply : ∀ (n : ℕ) [inst : NeZero n] (K : Type u_1) [inst_1 : Field K] [inst_2 : NumberField K]
  [hK : IsCyclotomicExtension {n} ℚ K] {m : ℕ} [inst_3 : NeZero m] (F : Type u_2) [inst_4 : Field F]
  [inst_5 : NumberField F] [hF : IsCyclotomicExtension {m} ℚ F] [inst_6 : Algebra F K] [inst_7 : IsGalois ℚ F]
  (h : m ∣ n) (σ : Gal(K/ℚ)),
  (IsCyclotomicExtension.Rat.galEquivZMod m F) (σ.restrictNormal F) =
    (ZMod.unitsMap h) ((IsCyclotomicExtension.Rat.galEquivZMod n K) σ)
-- Mathlib.CategoryTheory.Subterminal
CategoryTheory.instFaithfulSubterminalsSubterminalInclusion : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C], (CategoryTheory.subterminalInclusion C).Faithful
-- Mathlib.CategoryTheory.Preadditive.CommGrp_
_private.Mathlib.CategoryTheory.Preadditive.CommGrp_.0.CategoryTheory.Preadditive.monoidal_hom_ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.CartesianMonoidalCategory C] {X Y Z : C}
  {f g : CategoryTheory.MonoidalCategoryStruct.tensorObj X Y ⟶ Z},
  CategoryTheory.CategoryStruct.comp
        (CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CategoryStruct.id X) 0) f =
      CategoryTheory.CategoryStruct.comp
        (CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CategoryStruct.id X) 0) g →
    CategoryTheory.CategoryStruct.comp
          (CategoryTheory.CartesianMonoidalCategory.lift 0 (CategoryTheory.CategoryStruct.id Y)) f =
        CategoryTheory.CategoryStruct.comp
          (CategoryTheory.CartesianMonoidalCategory.lift 0 (CategoryTheory.CategoryStruct.id Y)) g →
      f = g
-- Lean.Meta.Tactic.Repeat
_private.Lean.Meta.Tactic.Repeat.0.Lean.Meta.repeat'Core.go.match_5.eq_2 : ∀ (motive : ℕ → Bool → List Lean.MVarId → List (List Lean.MVarId) → Array Lean.MVarId → Sort u_1) (n : ℕ) (p : Bool)
  (goals : List Lean.MVarId) (stk : List (List Lean.MVarId)) (acc : Array Lean.MVarId)
  (h_1 : (x : ℕ) → (p : Bool) → (acc : Array Lean.MVarId) → motive x p [] [] acc)
  (h_2 :
    (n : ℕ) →
      (p : Bool) →
        (goals : List Lean.MVarId) →
          (stk : List (List Lean.MVarId)) → (acc : Array Lean.MVarId) → motive n p [] (goals :: stk) acc)
  (h_3 :
    (n : ℕ) →
      (p : Bool) →
        (g : Lean.MVarId) →
          (goals : List Lean.MVarId) →
            (stk : List (List Lean.MVarId)) → (acc : Array Lean.MVarId) → motive n p (g :: goals) stk acc),
  (match n, p, [], goals :: stk, acc with
    | x, p, [], [], acc => h_1 x p acc
    | n, p, [], goals :: stk, acc => h_2 n p goals stk acc
    | n, p, g :: goals, stk, acc => h_3 n p g goals stk acc) =
    h_2 n p goals stk acc
-- Mathlib.Topology.Algebra.Group.Basic
/-- Eta-expanded form of `ContinuousAt.zpow` -/
ContinuousAt.fun_zpow : ∀ {G : Type w} {α : Type u} [inst : TopologicalSpace G] [inst_1 : Group G] [IsTopologicalGroup G]
  [inst_3 : TopologicalSpace α] {f : α → G} {x : α}, ContinuousAt f x → ∀ (z : ℤ), ContinuousAt (fun i => f i ^ z) x
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
NumberField.InfinitePlace.card_add_two_mul_card_eq_rank : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  NumberField.InfinitePlace.nrRealPlaces K + 2 * NumberField.InfinitePlace.nrComplexPlaces K = Module.finrank ℚ K
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
WeierstrassCurve.Jacobian.polynomialY.eq_1 : ∀ {R : Type r} [inst : CommRing R] (W' : WeierstrassCurve.Jacobian R),
  W'.polynomialY = (MvPolynomial.pderiv 1) W'.polynomial
-- Mathlib.Algebra.Group.Action.Sigma
Sigma.instSMul_mathlib : {ι : Type u_1} → {M : Type u_2} → {α : ι → Type u_4} → [(i : ι) → SMul M (α i)] → SMul M ((i : ι) × α i)
-- Mathlib.MeasureTheory.Group.Arithmetic
aemeasurable_neg_iff : ∀ {α : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {G : Type u_4} [inst : InvolutiveNeg G]
  [inst_1 : MeasurableSpace G] [MeasurableNeg G] {f : α → G}, AEMeasurable (fun x => -f x) μ ↔ AEMeasurable f μ
-- Mathlib.Tactic.Simproc.ExistsAndEq
ExistsAndEq.instInhabitedHypQ : Inhabited ExistsAndEq.HypQ
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- This is another convenient method to verify that a fork is a limit cone. It
only asks for a proof of facts that carry any mathematical content, and allows access to the
same `s` for all parts.  -/
CategoryTheory.Limits.Fork.IsLimit.mk' : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      {f g : X ⟶ Y} →
        (t : CategoryTheory.Limits.Fork f g) →
          ((s : CategoryTheory.Limits.Fork f g) →
              { l //
                CategoryTheory.CategoryStruct.comp l t.ι = s.ι ∧
                  ∀ {m : s.pt ⟶ t.pt}, CategoryTheory.CategoryStruct.comp m t.ι = s.ι → m = l }) →
            CategoryTheory.Limits.IsLimit t
-- Mathlib.Geometry.Diffeology.Basic
/-- A diffeology on `X`, given by the smooth functions (or "plots") from ℝⁿ to `X`.  -/
DiffeologicalSpace : Type u_1 → Type u_1
-- Mathlib.Algebra.DirectSum.LinearMap
LinearMap.mapsTo_biSup_of_mapsTo : ∀ {R : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {ι : Type u_4}
  {N : ι → Submodule R M} (s : Set ι) {f : Module.End R M},
  (∀ (i : ι), Set.MapsTo ⇑f ↑(N i) ↑(N i)) → Set.MapsTo ⇑f ↑(⨆ i ∈ s, N i) ↑(⨆ i ∈ s, N i)
-- Mathlib.Algebra.Homology.ShortComplex.Abelian
/-- The canonical `LeftHomologyData` of a short complex `S` in an abelian category, for
which the `H` field is `Abelian.coimage (kernel.ι S.g ≫ cokernel.π S.f)`.  -/
CategoryTheory.ShortComplex.LeftHomologyData.ofAbelian : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] → (S : CategoryTheory.ShortComplex C) → S.LeftHomologyData
-- Mathlib.Analysis.Normed.Module.Extr
/-- If `f : α → E` is a function such that `norm ∘ f` has a maximum along a filter `l` at a point
`c` and `y` is a vector on the same ray as `f c`, then the function `fun x => ‖f x + y‖` has
a maximum along `l` at `c`.  -/
IsMaxFilter.norm_add_sameRay : ∀ {α : Type u_1} {E : Type u_3} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : α → E} {l : Filter α}
  {c : α} {y : E}, IsMaxFilter (norm ∘ f) l c → SameRay ℝ (f c) y → IsMaxFilter (fun x => ‖f x + y‖) l c
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.addCommSemigroup : {R : Type u} → {M : Type v} → [AddCommSemigroup R] → [AddCommSemigroup M] → AddCommSemigroup (TrivSqZeroExt R M)
-- Mathlib.Topology.Semicontinuity.Defs
upperHemicontinuousOn_iff_frequently : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → Set β} {s : Set α},
  UpperHemicontinuousOn f s ↔
    ∀ x ∈ s, ∀ (t : Set β), IsClosed t → (∃ᶠ (x' : α) in nhdsWithin x s, (f x' ∩ t).Nonempty) → (f x ∩ t).Nonempty
-- Mathlib.Analysis.Convex.Gauge
/-- **Alias** of `Convex.setOfPred_gauge_le`. -/
Convex.gauge_le : ∀ {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Module ℝ E] {s : Set E},
  Convex ℝ s → 0 ∈ s → Absorbent ℝ s → ∀ (a : ℝ), Convex ℝ {x | gauge s x ≤ a}
-- Mathlib.CategoryTheory.MorphismProperty.Representable
/-- Given a relatively representable morphism `f : X ⟶ Y`, then for any `g : F.obj a ⟶ Y`,
`hf.fst g` denotes the first projection in the following diagram, given by the defining property
of `f` being relatively representable
```
hf.pullback g --F.map (hf.snd g)--> F.obj a
    |                                 |
hf.fst g                              g
    |                                 |
    v                                 v
    X -------------- f -------------> Y
```  -/
CategoryTheory.Functor.relativelyRepresentable.fst : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F : CategoryTheory.Functor C D} →
          {X Y : D} →
            {f : X ⟶ Y} → (hf : F.relativelyRepresentable f) → {a : C} → (g : F.obj a ⟶ Y) → F.obj (hf.pullback g) ⟶ X
-- Init.Control.Do
/-- A specialization of `Option.casesOn`.  -/
Break.runK : {α : Type u} → {β : Type v} → Option α → (Unit → β) → (α → β) → β
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.getKey?_insertMany_emptyWithCapacity_list_of_mem : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α] {l : List (α × β)}
  {k k' : α},
  (k == k') = true →
    List.Pairwise (fun a b => (a.1 == b.1) = false) l →
      k ∈ List.map Prod.fst l →
        (↑(Std.DHashMap.Internal.Raw₀.Const.insertMany Std.DHashMap.Internal.Raw₀.emptyWithCapacity l)).getKey? k' =
          some k
-- Mathlib.CategoryTheory.Sites.Coherent.SheafComparison
CategoryTheory.Presheaf.coherentExtensiveEquivalence_unitIso_hom_app_hom_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {A : Type u₃}
  [inst_1 : CategoryTheory.Category.{v₃, u₃} A] [inst_2 : CategoryTheory.Preregular C]
  [inst_3 : CategoryTheory.FinitaryExtensive C] [inst_4 : ∀ (X : C), CategoryTheory.Projective X]
  (X : CategoryTheory.Sheaf (CategoryTheory.coherentTopology C) A) (X_1 : Cᵒᵖ),
  (CategoryTheory.Presheaf.coherentExtensiveEquivalence.unitIso.hom.app X).hom.app X_1 =
    CategoryTheory.CategoryStruct.id (X.obj.obj X_1)
-- Mathlib.RingTheory.Filtration
/-- `Ideal.Filtration.submodule` as an `InfHom`.  -/
Ideal.Filtration.submoduleInfHom : {R : Type u_1} →
  (M : Type u_2) →
    [inst : CommRing R] →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] →
          (I : Ideal R) → InfHom (I.Filtration M) (Submodule (↥(reesAlgebra I)) (PolynomialModule R M))
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.NeWord.head.eq_def : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] (x x_1 : ι) (x_2 : Monoid.CoprodI.NeWord M x x_1),
  x_2.head =
    match x, x_1, x_2 with
    | x, .(x), Monoid.CoprodI.NeWord.singleton x_3 a => x_3
    | x, x_3, w₁.append _hne _w₂ => w₁.head
-- Mathlib.GroupTheory.Congruence.Hom
/-- Homomorphisms on the quotient of a monoid by a congruence relation `c` are equal if their
compositions with `c.mk'` are equal.  -/
Con.hom_ext : ∀ {M : Type u_1} {P : Type u_3} [inst : MulOneClass M] [inst_1 : MulOneClass P] {c : Con M} {f g : c.Quotient →* P},
  f.comp c.mk' = g.comp c.mk' → f = g
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
SimplexCategoryGenRel.standardσ_comp_standardσ_assoc : ∀ (L₁ L₂ : List ℕ) {m₁ m₂ m₃ : ℕ} (h : m₂ + L₁.length = m₁) (h' : m₃ + L₂.length = m₂) {Z : SimplexCategoryGenRel}
  (h_1 : SimplexCategoryGenRel.mk m₃ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (SimplexCategoryGenRel.standardσ L₁ h)
      (CategoryTheory.CategoryStruct.comp (SimplexCategoryGenRel.standardσ L₂ h') h_1) =
    CategoryTheory.CategoryStruct.comp (SimplexCategoryGenRel.standardσ (L₂ ++ L₁) ⋯) h_1
-- Std.Time.Date.Unit.Weekday
Std.Time.Weekday.instDecidableLtOrdinal : {x y : Std.Time.Weekday.Ordinal} → Decidable (x < y)
-- Mathlib.CategoryTheory.Sites.Precoverage
CategoryTheory.Precoverage.ext_iff : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {x y : CategoryTheory.Precoverage C},
  x = y ↔ x.coverings = y.coverings
-- Mathlib.RingTheory.RootsOfUnity.Basic
/-- Make an element of `rootsOfUnity` from a member of the base ring, and a proof that it has
a positive power equal to one.  -/
rootsOfUnity.mkOfPowEq : {M : Type u_1} → [inst : CommMonoid M] → (ζ : M) → {n : ℕ} → [NeZero n] → ζ ^ n = 1 → ↥(rootsOfUnity n M)
-- Mathlib.Order.Filter.AtTopBot.Map
OrderIso.comap_atBot : ∀ {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] (e : α ≃o β),
  Filter.comap (⇑e) Filter.atBot = Filter.atBot
-- Init.Data.UInt.Lemmas
UInt16.toNat.inj : ∀ {a b : UInt16}, a.toNat = b.toNat → a = b
-- Mathlib.Algebra.Group.Commute.Basic
AddCommute.neg_left_iff : ∀ {G : Type u_1} [inst : AddGroup G] {a b : G}, AddCommute (-a) b ↔ AddCommute a b
-- Mathlib.CategoryTheory.Bicategory.Functor.Prelax
CategoryTheory.PrelaxFunctor.id_toPrelaxFunctorStruct : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B],
  (CategoryTheory.PrelaxFunctor.id B).toPrelaxFunctorStruct = CategoryTheory.PrelaxFunctorStruct.id B
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.mk.congr_simp : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (inner inner_1 : Std.DHashMap.Raw α β)
  (e_inner : inner = inner_1) (wf : inner.WF), { inner := inner, wf := wf } = { inner := inner_1, wf := ⋯ }
-- Mathlib.CategoryTheory.Limits.Types.End
CategoryTheory.Limits.Types.chosenCoend_def : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J]
  {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J (Type (max w u)))},
  CategoryTheory.Limits.chosenCoend F = Quot (CategoryTheory.Limits.Types.coendRel F)
-- Mathlib.CategoryTheory.Abelian.Basic
/-- A category with finite products in which coimage-image comparisons are all isomorphisms
is a normal mono category.
 -/
CategoryTheory.Abelian.OfCoimageImageComparisonIsIso.isNormalMonoCategory : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasKernels C] [inst_3 : CategoryTheory.Limits.HasCokernels C]
  [∀ {X Y : C} (f : X ⟶ Y), CategoryTheory.IsIso (CategoryTheory.Abelian.coimageImageComparison f)]
  [CategoryTheory.Limits.HasFiniteProducts C], CategoryTheory.IsNormalMonoCategory C
-- Mathlib.Order.Monotone.Defs
StrictAnti.comp_strictMonoOn : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ] {g : β → γ}
  {f : α → β} {s : Set α}, StrictAnti g → StrictMonoOn f s → StrictAntiOn (g ∘ f) s
-- Init.Data.List.Erase
List.eraseIdx_ne_nil_iff : ∀ {α : Type u_1} {l : List α} {i : ℕ}, l.eraseIdx i ≠ [] ↔ 2 ≤ l.length ∨ l.length = 1 ∧ i ≠ 0
-- Mathlib.Util.CompileInductive
/-- Compiles the `sizeOf` auxiliary functions. It also recursively compiles any inductives required to
compile the `sizeOf` definition (because `sizeOf` definitions depend on `T.rec`).
 -/
Mathlib.Util.compileSizeOf : Lean.InductiveVal → Lean.RecursorVal → Lean.MetaM Unit
-- Mathlib.Analysis.SpecialFunctions.Log.Base
Real.floor_logb_natCast : ∀ {b : ℕ} {r : ℝ}, 0 ≤ r → ⌊Real.logb (↑b) r⌋ = Int.log b r
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.maxKey!_modify : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {k : α} {f : β → β},
  Std.ExtDTreeMap.Const.modify t k f ≠ ∅ →
    (Std.ExtDTreeMap.Const.modify t k f).maxKey! = if cmp t.maxKey! k = Ordering.eq then k else t.maxKey!
-- Mathlib.Topology.Basic
limUnder_of_not_tendsto : ∀ {X : Type u} {α : Type u_1} [inst : TopologicalSpace X] [hX : Nonempty X] {f : Filter α} {g : α → X},
  (¬∃ x, Filter.Tendsto g f (nhds x)) → f.limUnder g = Classical.choice hX
-- Mathlib.Topology.Order.LeftRightNhds
/-- A set is a neighborhood of `a` within `[a, +∞)` if and only if it contains an interval `[a, u]`
with `a < u`.  -/
mem_nhdsGE_iff_exists_Icc_subset : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [NoMaxOrder α]
  [DenselyOrdered α] {a : α} {s : Set α}, s ∈ nhdsWithin a (Set.Ici a) ↔ ∃ u, a < u ∧ Set.Icc a u ⊆ s
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
/-- A measurable embedding is injective.  -/
MeasurableEmbedding.injective : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {f : α → β},
  MeasurableEmbedding f → Function.Injective f
-- Batteries.Data.String.Lemmas
String.utf8Len_nil : String.utf8Len [] = 0
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.SolverExtension.getStateCore : {σ : Type} → Lean.Meta.Grind.SolverExtension σ → Lean.Meta.Grind.Goal → IO σ
-- Mathlib.Geometry.Manifold.Diffeomorph
/-- Interpret a diffeomorphism as a `ContMDiffMap`.  -/
Diffeomorph.toContMDiffMap : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {E' : Type u_3} →
            [inst_3 : NormedAddCommGroup E'] →
              [inst_4 : NormedSpace 𝕜 E'] →
                {H : Type u_5} →
                  [inst_5 : TopologicalSpace H] →
                    {H' : Type u_6} →
                      [inst_6 : TopologicalSpace H'] →
                        {I : ModelWithCorners 𝕜 E H} →
                          {I' : ModelWithCorners 𝕜 E' H'} →
                            {M : Type u_9} →
                              [inst_7 : TopologicalSpace M] →
                                [inst_8 : ChartedSpace H M] →
                                  {M' : Type u_10} →
                                    [inst_9 : TopologicalSpace M'] →
                                      [inst_10 : ChartedSpace H' M'] →
                                        {n : WithTop ℕ∞} → Diffeomorph I I' M M' n → ContMDiffMap I I' M M' n
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.get!_diff : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {k : α} [inst_1 : Inhabited (β k)],
  (t₁ \ t₂).get! k = if k ∈ t₂ then default else t₁.get! k
-- Lean.CoreM
Lean.Core.Context.maxRecDepth : Lean.Core.Context → ℕ
-- Init.Data.SInt.Bitwise
Int64.toInt32_xor : ∀ (a b : Int64), (a ^^^ b).toInt32 = a.toInt32 ^^^ b.toInt32
-- Lean.Meta.Tactic.Grind.CheckResult
Lean.Meta.Grind.CheckResult.noConfusionType : Sort v✝ → Lean.Meta.Grind.CheckResult → Lean.Meta.Grind.CheckResult → Sort v✝
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.instUniqueOfIsEmpty : {α : Type u} → [IsEmpty α] → Unique (FreeAddGroup α)
-- Mathlib.Data.Set.Defs
/-- The property `s.Nonempty` expresses the fact that the set `s` is not empty. It should be used
in theorem assumptions instead of `∃ x, x ∈ s` or `s ≠ ∅` as it gives access to a nice API thanks
to the dot notation.  -/
Set.Nonempty : {α : Type u} → Set α → Prop
-- Mathlib.GroupTheory.Index
Subgroup.instFiniteIndexTop : ∀ {G : Type u_1} [inst : Group G], ⊤.FiniteIndex
-- Mathlib.NumberTheory.Cyclotomic.Gal
IsCyclotomicExtension.autEquivPow_symm_apply : ∀ {n : ℕ} [inst : NeZero n] {K : Type u_1} [inst_1 : Field K] (L : Type u_2) [inst_2 : CommRing L] [inst_3 : IsDomain L]
  [inst_4 : Algebra K L] [inst_5 : IsCyclotomicExtension {n} K L] (h : Irreducible (Polynomial.cyclotomic n K))
  (t : (ZMod n)ˣ),
  (IsCyclotomicExtension.autEquivPow L h).symm t =
    (IsPrimitiveRoot.powerBasis K ⋯).equivOfMinpoly (IsPrimitiveRoot.powerBasis K ⋯) ⋯
-- Std.Data.DTreeMap.Internal.Queries
/-- Implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.minEntry? : {α : Type u} → {β : α → Type v} → Std.DTreeMap.Internal.Impl α β → Option ((a : α) × β a)
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.smul_monomial : ∀ {R : Type u_1} (n : ℕ) [inst : Semiring R] {S : Type u_5} [inst_1 : Semiring S] [inst_2 : Module S R] (a : S) (b : R),
  a • (SkewPolynomial.monomial n) b = (SkewPolynomial.monomial n) (a • b)
-- Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
/-- The glue data of topological spaces associated to a family of glue data of PresheafedSpaces.  -/
AlgebraicGeometry.PresheafedSpace.GlueData.toTopGlueData : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → AlgebraicGeometry.PresheafedSpace.GlueData C → TopCat.GlueData
-- Mathlib.Data.Matrix.Diagonal
Matrix.transpose_eq_one : ∀ {n : Type u_3} {α : Type v} [inst : DecidableEq n] [inst_1 : Zero α] [inst_2 : One α] {M : Matrix n n α},
  M.transpose = 1 ↔ M = 1
-- Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
setIntegral_Ioi_zero_cpow : ∀ (s : ℂ), ∫ (x : ℝ) in Set.Ioi 0, ↑x ^ s = 0
-- Lean.SubExpr
Lean.instInhabitedSubExpr.default : Lean.SubExpr
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.stdSimplex.face_eq_ofSimplex : ∀ {n : ℕ} (S : Finset (Fin (n + 1))) (m : ℕ) (e : Fin (m + 1) ≃o ↥S),
  SSet.stdSimplex.face S =
    SSet.Subcomplex.ofSimplex
      (SSet.stdSimplex.objMk ((OrderHom.Subtype.val fun x => x ∈ S).comp e.toOrderEmbedding.toOrderHom))
-- Aesop.ElabM
Aesop.ElabM.Context.forErasing : Lean.MVarId → Aesop.ElabM.Context