mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.CommGrp_
CategoryTheory.CommGrp.toCommMon_X : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (A : CategoryTheory.CommGrp C), A.toCommMon.X = A.X
-- Mathlib.MeasureTheory.Group.Measure
/-- A convenience wrapper for `MeasureTheory.Measure.isAddHaarMeasure_map`.  -/
ContinuousAddEquiv.isAddHaarMeasure_map : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : AddGroup G] [inst_2 : TopologicalSpace G]
  (μ : MeasureTheory.Measure G) [μ.IsAddHaarMeasure] [BorelSpace G] [IsTopologicalAddGroup G] {H : Type u_3}
  [inst_6 : AddGroup H] [inst_7 : TopologicalSpace H] [inst_8 : MeasurableSpace H] [BorelSpace H]
  [IsTopologicalAddGroup H] (e : G ≃ₜ+ H), (MeasureTheory.Measure.map (⇑e) μ).IsAddHaarMeasure
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey?_eq_some_of_contains : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  {k : α}, t.contains k = true → t.getKey? k = some k
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
MeasureTheory.aecover_Icc_of_Ico : ∀ {α : Type u_1} {ι : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {l : Filter ι}
  [inst_1 : LinearOrder α] [inst_2 : TopologicalSpace α] [OrderClosedTopology α] [OpensMeasurableSpace α] {a b : ι → α}
  {A B : α} [MeasureTheory.NullSingletonClass μ],
  Filter.Tendsto a l (nhds A) →
    Filter.Tendsto b l (nhds B) → MeasureTheory.AECover (μ.restrict (Set.Icc A B)) l fun i => Set.Ico (a i) (b i)
-- Mathlib.Algebra.Category.Semigrp.Basic
AddSemigrp.instCoeSortType : CoeSort AddSemigrp (Type u)
-- Mathlib.Order.Filter.Basic
Filter.eventually_of_mem : ∀ {α : Type u} {f : Filter α} {P : α → Prop} {U : Set α}, U ∈ f → (∀ x ∈ U, P x) → ∀ᶠ (x : α) in f, P x
-- Mathlib.CategoryTheory.Monoidal.Ring
CategoryTheory.Hom.mul_add : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {R : C} [inst_3 : CategoryTheory.RingObj R] {X : C} (a b c : X ⟶ R),
  a * (b + c) = a * b + a * c
-- Mathlib.Topology.MetricSpace.ThickenedIndicator
/-- Pointwise, the multiplicative indicators of δ-thickenings of a set eventually coincide
with the multiplicative indicator of the set as δ>0 tends to zero.  -/
mulIndicator_thickening_eventually_eq_mulIndicator_closure : ∀ {α : Type u_1} [inst : PseudoEMetricSpace α] {β : Type u_2} [inst_1 : One β] (f : α → β) (E : Set α) (x : α),
  ∀ᶠ (δ : ℝ) in nhdsWithin 0 (Set.Ioi 0), (Metric.thickening δ E).mulIndicator f x = (closure E).mulIndicator f x
-- Mathlib.Dynamics.Flow
Flow.mk.injEq : ∀ {τ : Type u_1} {α : Type u_2} [inst : TopologicalSpace τ] [inst_1 : TopologicalSpace α] [inst_2 : AddZero τ]
  (toFun : τ → α → α) (cont' : Continuous (Function.uncurry toFun))
  (map_add' : ∀ (t₁ t₂ : τ) (x : α), toFun (t₁ + t₂) x = toFun t₁ (toFun t₂ x)) (map_zero' : ∀ (x : α), toFun 0 x = x)
  (toFun_1 : τ → α → α) (cont'_1 : Continuous (Function.uncurry toFun_1))
  (map_add'_1 : ∀ (t₁ t₂ : τ) (x : α), toFun_1 (t₁ + t₂) x = toFun_1 t₁ (toFun_1 t₂ x))
  (map_zero'_1 : ∀ (x : α), toFun_1 0 x = x),
  ({ toFun := toFun, cont' := cont', map_add' := map_add', map_zero' := map_zero' } =
      { toFun := toFun_1, cont' := cont'_1, map_add' := map_add'_1, map_zero' := map_zero'_1 }) =
    (toFun = toFun_1)
-- Mathlib.CategoryTheory.Join.Basic
/-- A situational lemma to help putting identities in the form `(inclRight _ _).map _` when using
`homInduction`.  -/
CategoryTheory.Join.id_right : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (d : D),
  CategoryTheory.CategoryStruct.id (CategoryTheory.Join.right d) =
    (CategoryTheory.Join.inclRight C D).map (CategoryTheory.CategoryStruct.id d)
-- Mathlib.Algebra.ContinuedFractions.Computation.Basic
GenContFract.IntFractPair.mk : {K : Type u_1} → ℤ → K → GenContFract.IntFractPair K
-- Std.Data.HashMap.Lemmas
Std.HashMap.Equiv.of_forall_getKey_eq_of_forall_getElem?_eq : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α],
  (∀ (k : α) (hk : k ∈ m₁) (hk' : k ∈ m₂), m₁.getKey k hk = m₂.getKey k hk') →
    (∀ (k : α), m₁[k]? = m₂[k]?) → m₁.Equiv m₂
-- Init.Grind.Interactive
/-- `fail_if_success t` fails if the tactic `t` succeeds.  -/
Lean.Parser.Tactic.Grind.failIfSuccess : Lean.ParserDescr
-- Mathlib.NumberTheory.LocalField.Basic
IsNonarchimedeanLocalField.instCompleteSpaceSubtypeMemSubringIntegerValueGroupWithZeroValuation : ∀ (K : Type u_1) [inst : Field K] [inst_1 : ValuativeRel K] [inst_2 : UniformSpace K] [IsUniformAddGroup K]
  [IsNonarchimedeanLocalField K], CompleteSpace ↥(ValuativeRel.valuation K).integer
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.instCommSemigroupOfContinuousMul.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : CommSemigroup β]
  [inst_3 : ContinuousMul β],
  ContinuousMap.instCommSemigroupOfContinuousMul =
    { toSemigroup := ContinuousMap.instSemigroupOfContinuousMul, mul_comm := ⋯ }
-- Init.Data.SInt.Lemmas
Int32.toBitVec_one : Int32.toBitVec 1 = 1#32
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKey_insert_self : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] (h : (↑m).WF) {k : α} {v : β k}, (m.insert k v).getKey k ⋯ = k
-- Mathlib.Data.List.PeriodicityLemma
List.HasPeriod.infix : ∀ {α : Type u_1} {u w : List α} {p : ℕ}, w.HasPeriod p → u <:+: w → u.HasPeriod p
-- Mathlib.Order.Comparable
CompRel.decidableRel : {α : Type u_1} → {r : α → α → Prop} → [DecidableRel r] → DecidableRel (CompRel r)
-- Mathlib.CategoryTheory.Sites.Sheafification
CategoryTheory.sheafifyLift_id_toSheafify : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} D] [inst_2 : CategoryTheory.HasWeakSheafify J D]
  {P : CategoryTheory.Functor Cᵒᵖ D} (hP : CategoryTheory.Presheaf.IsSheaf J P),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.sheafifyLift J (CategoryTheory.CategoryStruct.id P) hP)
      (CategoryTheory.toSheafify J P) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.sheafify J P)
-- Mathlib.Data.Option.Basic
Option.map_comp_some : ∀ {α : Type u_1} {β : Type u_2} (f : α → β), Option.map f ∘ some = some ∘ f
-- Lean.Linter.Sets
/-- `registerSet` wraps `registerOption` by setting relevant values.  -/
Lean.Linter.registerSet : Lean.Name → autoParam Lean.Name Lean.Linter.registerSet._auto_1 → IO (Lean.Option Bool)
-- Mathlib.CategoryTheory.Monoidal.Free.Coherence
/-- Auxiliary definition for `normalizeIso`.  -/
CategoryTheory.FreeMonoidalCategory.normalizeIsoAux : (C : Type u) →
  (X : CategoryTheory.FreeMonoidalCategory C) →
    (CategoryTheory.FreeMonoidalCategory.tensorFunc C).obj X ≅ (CategoryTheory.FreeMonoidalCategory.normalize' C).obj X
-- Mathlib.Analysis.RCLike.Basic
RCLike.ofReal_mul_neg_iff : ∀ {K : Type u_1} [inst : RCLike K] (x : ℝ) (z : K), ↑x * z < 0 ↔ x < 0 ∧ 0 < z ∨ 0 < x ∧ z < 0
-- Mathlib.NumberTheory.MulChar.Basic
MulChar.toUnitHom_eq : ∀ {R : Type u_1} [inst : CommMonoid R] {R' : Type u_2} [inst_1 : CommMonoidWithZero R'] (χ : MulChar R R'),
  χ.toUnitHom = MulChar.equivToUnitHom χ
-- Mathlib.Algebra.Group.Subgroup.Defs
/-- **Alias** of `Subgroup.normalizer`.

---

The `normalizer` of `S` is the subgroup of `G` whose elements satisfy `g * S * g⁻¹ = S`.
When `S` is a subgroup, this is the largest subgroup of `G` inside which `S` is normal.  -/
Subgroup.setNormalizer : {G : Type u_1} → [inst : Group G] → Set G → Subgroup G
-- Mathlib.Algebra.Notation.Indicator
Set.indicator_apply_eq_self : ∀ {α : Type u_1} {M : Type u_3} [inst : Zero M] {s : Set α} {f : α → M} {a : α}, s.indicator f a = f a ↔ a ∉ s → f a = 0
-- Mathlib.Data.List.Sym
_private.Mathlib.Data.List.Sym.0.List.sym2.match_1.eq_2 : ∀ {α : Type u_1} (motive : List α → Sort u_2) (x : α) (xs : List α) (h_1 : Unit → motive [])
  (h_2 : (x : α) → (xs : List α) → motive (x :: xs)),
  (match x :: xs with
    | [] => h_1 ()
    | x :: xs => h_2 x xs) =
    h_2 x xs
-- Mathlib.AlgebraicGeometry.Morphisms.Immersion
AlgebraicGeometry.IsImmersion.instLocallyOfFiniteType : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsImmersion f],
  AlgebraicGeometry.LocallyOfFiniteType f
-- Mathlib.Tactic.FunProp.Types
Mathlib.Meta.FunProp.GeneralTheorem.mk.injEq : ∀ (funPropName thmName : Lean.Name)
  (keys : List (Lean.Meta.RefinedDiscrTree.Key × Lean.Meta.RefinedDiscrTree.LazyEntry)) (priority : ℕ)
  (funPropName_1 thmName_1 : Lean.Name)
  (keys_1 : List (Lean.Meta.RefinedDiscrTree.Key × Lean.Meta.RefinedDiscrTree.LazyEntry)) (priority_1 : ℕ),
  ({ funPropName := funPropName, thmName := thmName, keys := keys, priority := priority } =
      { funPropName := funPropName_1, thmName := thmName_1, keys := keys_1, priority := priority_1 }) =
    (funPropName = funPropName_1 ∧ thmName = thmName_1 ∧ keys = keys_1 ∧ priority = priority_1)
-- Init.Data.List.Lemmas
List.foldlRecOn_cons : ∀ {β : Type u_1} {α : Type u_2} {b : β} {x : α} {l : List α} {motive : β → Sort u_3} {op : β → α → β} (hb : motive b)
  (hl : (b : β) → motive b → (a : α) → a ∈ x :: l → motive (op b a)),
  List.foldlRecOn (x :: l) op hb hl = List.foldlRecOn l op (hl b hb x ⋯) fun b c a m => hl b c a ⋯
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.withCheapCasesOnly : {α : Type} → Lean.Meta.Grind.GrindM α → Lean.Meta.Grind.GrindM α
-- Lean.Elab.ConfigEval.DeriveEvalConfigItem
/-- Finds a handler that applies to this key.
Returns the trie key and the handler.

If `kind` is `exact` then it returns the handler that would actually apply,
and if it is `wildcard` then it returns the wildcard handler corresponding to that
key if an `exact` handler would also apply.
 -/
_private.Lean.Elab.ConfigEval.DeriveEvalConfigItem.0.Lean.Elab.ConfigEval.HandlerTrie.find? : Lean.Elab.ConfigEval.HandlerTrie✝ →
  Lean.Name →
    Lean.Elab.ConfigEval.EvalConfigItemHandlerKind → Option (Lean.Name × Lean.Elab.ConfigEval.EvalConfigItemHandler)
-- Mathlib.LinearAlgebra.Quotient.Defs
Submodule.Quotient.distribSMul : {R : Type u_1} →
  {M : Type u_2} →
    [inst : Ring R] → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → (P : Submodule R M) → DistribSMul R (M ⧸ P)
-- Mathlib.Algebra.Group.Hom.Defs
iterate_map_inv : ∀ {M : Type u_10} {F : Type u_11} [inst : Group M] [inst_1 : FunLike F M M] [MonoidHomClass F M M] (f : F) (n : ℕ)
  (x : M), (⇑f)^[n] x⁻¹ = ((⇑f)^[n] x)⁻¹
-- Mathlib.Geometry.Manifold.ContMDiff.Atlas
contMDiffAt_symm_of_mem_maximalAtlas : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {n : WithTop ℕ∞} {e : OpenPartialHomeomorph M H} {x : H},
  e ∈ IsManifold.maximalAtlas I n M → x ∈ e.target → ContMDiffAt I I n (↑e.symm) x
-- Mathlib.Algebra.Module.Presentation.Cokernel
/-- a lifting of `f (g₁ i)` in `pres₂.G →₀ A`  -/
Module.Presentation.CokernelData.lift : {A : Type u} →
  [inst : Ring A] →
    {M₁ : Type v₁} →
      {M₂ : Type v₂} →
        [inst_1 : AddCommGroup M₁] →
          [inst_2 : Module A M₁] →
            [inst_3 : AddCommGroup M₂] →
              [inst_4 : Module A M₂] →
                {pres₂ : Module.Presentation A M₂} →
                  {f : M₁ →ₗ[A] M₂} → {ι : Type w₁} → {g₁ : ι → M₁} → pres₂.CokernelData f g₁ → ι → pres₂.G →₀ A
-- Mathlib.Order.WithBot
/-- A universe-polymorphic version of `EquivFunctor.mapEquiv WithBot e`.  -/
Equiv.withBotCongr : {α : Type u_1} → {β : Type u_2} → α ≃ β → WithBot α ≃ WithBot β
-- Mathlib.Control.Lawful
/-- A copy of `LawfulFunctor.map_const` for `StateT` that holds even if `m` is not lawful.  -/
StateT.map_const : ∀ {σ : Type u} {m : Type u → Type v} {α β : Type u} [inst : Monad m], Functor.mapConst = Functor.map ∘ Function.const β
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get_erase : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k a : α} {h' : a ∈ m.erase k},
  Std.DHashMap.Const.get (m.erase k) a h' = Std.DHashMap.Const.get m a ⋯
-- Init.Grind.Interactive
Lean.Parser.Tactic.Grind.«grind_filterGen>_» : Lean.ParserDescr
-- Init.Data.Array.Lemmas
Array.appendList_cons : ∀ {α : Type u_1} {xs : Array α} {a : α} {l : List α}, xs ++ a :: l = xs.push a ++ l
-- Std.Internal.UV.System
/-- Gets the path to the temporary directory.
 -/
Std.Internal.UV.System.osTmpdir : IO String
-- Mathlib.Algebra.Order.Archimedean.Class
/-- An open ball defined by `MulArchimedeanClass.subgroup` of `UpperSet.Ioi c`.
For `c = ⊤`, we assign the junk value `⊥`.  -/
MulArchimedeanClass.ballSubgroup : {M : Type u_1} →
  [inst : CommGroup M] → [inst_1 : LinearOrder M] → [inst_2 : IsOrderedMonoid M] → MulArchimedeanClass M → Subgroup M
-- Mathlib.Util.Export
Lean.Export.Alloc.map : {α : Type u_1} → [inst : BEq α] → [inst_1 : Hashable α] → Lean.Export.Alloc α → Std.HashMap α ℕ
-- Mathlib.Data.Nat.Factorization.Root
Nat.floorRoot_pow_self : ∀ {n : ℕ}, n ≠ 0 → ∀ (a : ℕ), n.floorRoot (a ^ n) = a
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenNormalSubgroup.instInfOpenNormalSubgroup.eq_1 : ∀ {G : Type u} [inst : Group G] [inst_1 : TopologicalSpace G],
  OpenNormalSubgroup.instInfOpenNormalSubgroup =
    { min := fun U V => { toOpenSubgroup := U.toOpenSubgroup ⊓ V.toOpenSubgroup, isNormal' := ⋯ } }
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.binaryProductTriangle_mor₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ] (X₁ X₂ : C)
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.Limits.HasBinaryProduct X₁ X₂],
  (CategoryTheory.Pretriangulated.binaryProductTriangle X₁ X₂).mor₁ =
    CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.id X₁) 0
-- Mathlib.Geometry.RingedSpace.PresheafedSpace
AlgebraicGeometry.PresheafedSpace.ofRestrict_base : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {U : TopCat} (X : AlgebraicGeometry.PresheafedSpace C)
  {f : U ⟶ ↑X} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)), (X.ofRestrict h).base = f
-- Mathlib.Logic.Unique
uniqueElim_default : ∀ {ι : Sort u_2} {α : ι → Sort u_3} {x : Unique ι} (x_1 : α default), uniqueElim x_1 default = x_1
-- Batteries.Data.Nat.Bitwise.Lemmas
Nat.xor_left_injective : ∀ {x : ℕ}, Function.Injective fun x_1 => x_1 ^^^ x
-- Mathlib.RingTheory.Length
RelHom.mk.congr_simp : ∀ {α : Type u_5} {β : Type u_6} {r : α → α → Prop} {s : β → β → Prop} (toFun toFun_1 : α → β)
  (e_toFun : toFun = toFun_1) (map_rel' : ∀ {a b : α}, r a b → s (toFun a) (toFun b)),
  { toFun := toFun, map_rel' := map_rel' } = { toFun := toFun_1, map_rel' := ⋯ }
-- Init.Data.Range.Polymorphic.Lemmas
_private.Init.Data.Range.Polymorphic.Lemmas.0.List.forIn'_cons.match_1.eq_1 : ∀ {β : Type u_1} (motive : ForInStep β → Sort u_2) (b : β) (h_1 : (b : β) → motive (ForInStep.done b))
  (h_2 : (b : β) → motive (ForInStep.yield b)),
  (match ForInStep.done b with
    | ForInStep.done b => h_1 b
    | ForInStep.yield b => h_2 b) =
    h_1 b
-- Mathlib.LinearAlgebra.Matrix.Action
Matrix.instSMulCommClassMulOppositeForallOfIsScalarTower : ∀ {n : Type u_1} {R : Type u_2} {S : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : Semiring R]
  [inst_3 : DistribSMul S R] [IsScalarTower S R R], SMulCommClass (Matrix n n R)ᵐᵒᵖ S (n → R)
-- Mathlib.Data.Set.Semiring
Set.up_one : ∀ {α : Type u_1} [inst : One α], Set.up 1 = 1
-- Mathlib.Algebra.BigOperators.Fin
Fin.prod_univ_two : ∀ {M : Type u_2} [inst : CommMonoid M] (f : Fin 2 → M), ∏ i, f i = f 0 * f 1
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
/-- The cosine of an angle in a right-angled triangle as a ratio of sides, version subtracting
vectors.  -/
InnerProductGeometry.cos_angle_sub_of_inner_eq_zero : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
  inner ℝ x y = 0 → Real.cos (InnerProductGeometry.angle x (x - y)) = ‖x‖ / ‖x - y‖
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.isoRestrict_inv_ofRestrict : ∀ {X Y : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Y) [H : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion f],
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.isoRestrict f).inv f =
    Y.ofRestrict ⋯
-- Mathlib.Algebra.Module.LocalizedModule.Basic
_private.Mathlib.Algebra.Module.LocalizedModule.Basic.0.LocalizedModule.smul_zero_aux : ∀ {R : Type u} [inst : CommSemiring R] {S : Submonoid R} {M : Type v} [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {T : Type u_1} [inst_3 : CommSemiring T] [inst_4 : Algebra R T] [inst_5 : IsLocalization S T] (x : T), x • 0 = 0
-- Mathlib.AlgebraicTopology.SimplicialSet.Nonsingular
SSet.Nonsingular.mono' : ∀ {X : SSet} [X.Nonsingular] {n : ℕ}, ∀ x ∈ X.nonDegenerate n, CategoryTheory.Mono (SSet.yonedaEquiv.symm x)
-- Mathlib.RepresentationTheory.Continuous.Basic
ContRepresentation.Equiv.coe_toContIntertwiningMap : ∀ {R : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Monoid G] [inst_1 : Ring R]
  [inst_2 : AddCommGroup V] [inst_3 : TopologicalSpace V] [inst_4 : IsTopologicalAddGroup V] [inst_5 : Module R V]
  [inst_6 : AddCommGroup W] [inst_7 : TopologicalSpace W] [inst_8 : IsTopologicalAddGroup W] [inst_9 : Module R W]
  {ρ : ContRepresentation R G V} {σ : ContRepresentation R G W} (φ : ρ.Equiv σ), ⇑↑φ = ⇑φ
-- Init.Data.BitVec.Lemmas
BitVec.succ_mul : ∀ {w : ℕ} {x y : BitVec w}, (x + 1#w) * y = x * y + y
-- Mathlib.Data.Ordmap.Ordset
Ordset.instInhabited : {α : Type u_1} → [inst : Preorder α] → Inhabited (Ordset α)
-- Mathlib.GroupTheory.Commutator.Basic
AddSubgroup.Normal.quotient_commutative_iff_addCommutator_le : ∀ {G : Type u_1} [inst : AddGroup G] {N : AddSubgroup G} [inst_1 : N.Normal],
  IsAddCommutative (G ⧸ N) ↔ addCommutator G ≤ N
-- Mathlib.CategoryTheory.Sites.Over
CategoryTheory.GrothendieckTopology.overMapPullbackCongr.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (A : Type u')
  [inst_1 : CategoryTheory.Category.{v', u'} A] {X Y : C} {f g : X ⟶ Y} (h : f = g),
  J.overMapPullbackCongr A h = J.overMapPullbackCongr A h
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
/-- Coercion of an element of `K` into the adic completion.  -/
IsDedekindDomain.HeightOneSpectrum.adicCompletion.instCoe : {R : Type u_1} →
  [inst : CommRing R] →
    [inst_1 : IsDedekindDomain R] →
      (K : Type u_2) →
        [inst_2 : Field K] →
          [inst_3 : Algebra R K] →
            [inst_4 : IsFractionRing R K] →
              (v : IsDedekindDomain.HeightOneSpectrum R) → Coe K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)
-- Mathlib.AlgebraicTopology.EilenbergSteenrod
TopPair.HomologyPretheory.comp_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} {X Y Z : TopPair.HomologyPretheory C c} (f : X.Hom Y) (g : Y.Hom Z) (i : ι),
  (CategoryTheory.CategoryStruct.comp f g).hom i =
    CategoryTheory.CategoryStruct.comp (X.iso i).hom
      (CategoryTheory.CategoryStruct.comp
        (TopPair.incl.whiskerLeft ((fun x => CategoryTheory.CategoryStruct.comp (f.homₚ x) (g.homₚ x)) i))
        (Z.iso i).inv)
-- Mathlib.Order.CountableDenseLinearOrder
/-- Suppose `α` is a nonempty dense linear order without endpoints, and
suppose `lo`, `hi`, are finite subsets with all of `lo` strictly before `hi`.
Then there is an element of `α` strictly between `lo` and `hi`.  -/
Order.exists_between_finsets : ∀ {α : Type u_1} [inst : LinearOrder α] [DenselyOrdered α] [NoMinOrder α] [NoMaxOrder α] [nonem : Nonempty α]
  (lo hi : Finset α), (∀ x ∈ lo, ∀ y ∈ hi, x < y) → ∃ m, (∀ x ∈ lo, x < m) ∧ ∀ y ∈ hi, m < y
-- Batteries.Data.HashMap.Basic
/-- **Alias** of `LawfulHashable`. -/
Batteries.HashMap.LawfulHashable : (α : Type u) → [BEq α] → [Hashable α] → Prop
-- Mathlib.Condensed.Discrete.Colimit
Condensed.locallyConstantIsoFinYoneda_hom_app : ∀ (F : CategoryTheory.Functor Profiniteᵒᵖ (Type (u + 1))) (X : FintypeCatᵒᵖ),
  (Condensed.locallyConstantIsoFinYoneda F).hom.app X = TypeCat.ofHom fun f => ⇑f
-- Lean.Elab.Tactic.Simp
Lean.Meta.DSimp.ConfigWithOptions.mk.injEq : ∀ (config : Lean.Meta.DSimp.Config) (userConfig : Lean.Options) (config_1 : Lean.Meta.DSimp.Config)
  (userConfig_1 : Lean.Options),
  ({ config := config, userConfig := userConfig } = { config := config_1, userConfig := userConfig_1 }) =
    (config = config_1 ∧ userConfig = userConfig_1)
-- Mathlib.Analysis.Asymptotics.TVS
Asymptotics.isBigOTVS_pi : ∀ {α : Type u_1} {𝕜 : Type u_3} {F : Type u_5} [inst : NontriviallyNormedField 𝕜] [inst_1 : AddCommGroup F]
  [inst_2 : TopologicalSpace F] [inst_3 : Module 𝕜 F] {l : Filter α} {g : α → F} {ι : Type u_7} {E : ι → Type u_8}
  [inst_4 : (i : ι) → AddCommGroup (E i)] [inst_5 : (i : ι) → Module 𝕜 (E i)]
  [inst_6 : (i : ι) → TopologicalSpace (E i)] [∀ (i : ι), ContinuousSMul 𝕜 (E i)] {f : α → (i : ι) → E i},
  f =O[𝕜; l] g ↔ ∀ (i : ι), (fun x => f x i) =O[𝕜; l] g
-- Mathlib.Algebra.Lie.Nilpotent
LieSubmodule.isNilpotent_iff_exists_self_le_ucs : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] (N : LieSubmodule R L M)
  [inst_6 : LieModule R L M], LieModule.IsNilpotent L ↥N ↔ ∃ k, N ≤ LieSubmodule.ucs k ⊥
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.minEntryD.eq_3 : ∀ {α : Type u} {β : Type v} (x : α × β) (size : ℕ) (k : α) (v : β) (size_1 : ℕ) (k_1 : α) (v_1 : β)
  (l r r_1 : Std.DTreeMap.Internal.Impl α fun x => β),
  Std.DTreeMap.Internal.Impl.Const.minEntryD
      (Std.DTreeMap.Internal.Impl.inner size k v (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r) r_1) x =
    Std.DTreeMap.Internal.Impl.Const.minEntryD (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r) x
-- Lean.Meta.DiscrTree.Main
_private.Lean.Meta.DiscrTree.Main.0.Lean.Meta.DiscrTree.getMatchWithExtra.go : {α : Type} → Lean.Meta.DiscrTree α → Lean.Expr → ℕ → Array (α × ℕ) → Lean.MetaM (Array (α × ℕ))
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsLimit.equivIsoLimit_symm_apply : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {r t : CategoryTheory.Limits.Cone F} (i : r ≅ t)
  (P : CategoryTheory.Limits.IsLimit t), (CategoryTheory.Limits.IsLimit.equivIsoLimit i).symm P = P.ofIsoLimit i.symm
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
_private.Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic.0.termX : Lean.ParserDescr
-- Mathlib.Data.Real.ConjExponents
/-- The conjugate exponent of `p` is `q = 1 + (p - 1)⁻¹`, so that `p⁻¹ + q⁻¹ = 1`.  -/
ENNReal.conjExponent : ENNReal → ENNReal
-- Mathlib.RingTheory.Ideal.Prod
Ideal.map_fst_prod : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] (I : Ideal R) (J : Ideal S),
  Ideal.map (RingHom.fst R S) (I.prod J) = I
-- Mathlib.CategoryTheory.WithTerminal.Basic
/-- Composition of morphisms for `WithInitial C`.  -/
CategoryTheory.WithInitial.comp : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → {X Y Z : CategoryTheory.WithInitial C} → X.Hom Y → Y.Hom Z → X.Hom Z
-- Mathlib.Algebra.Group.TypeTags.Hom
MonoidHom.coe_toAdditiveRight : ∀ {α : Type u_3} {β : Type u_4} [inst : AddZeroClass α] [inst_1 : MulOneClass β] (f : Multiplicative α →* β),
  ⇑(MonoidHom.toAdditiveRight f) = ⇑Additive.ofMul ∘ ⇑f ∘ ⇑Multiplicative.ofAdd
-- Mathlib.Tactic.Linter.UnusedTactic
/-- A list of blocklisted syntax kinds, which are expected to have subterms that contain
unused tactics.
 -/
_private.Mathlib.Tactic.Linter.UnusedTactic.0.Mathlib.Linter.UnusedTactic.ignoreTacticKindsRef : IO.Ref Lean.NameHashSet