mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.End
CategoryTheory.Limits.coend.map_comp : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {C : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} C]
  {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)} [inst_2 : CategoryTheory.Limits.HasCoend F]
  {F' : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)} [inst_3 : CategoryTheory.Limits.HasCoend F']
  (f : F ⟶ F') {F'' : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)}
  [inst_4 : CategoryTheory.Limits.HasCoend F''] (g : F' ⟶ F''),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coend.map f) (CategoryTheory.Limits.coend.map g) =
    CategoryTheory.Limits.coend.map (CategoryTheory.CategoryStruct.comp f g)
-- Mathlib.Algebra.Category.Grp.EquivalenceGroupAddGroup
commGroupAddCommGroupEquivalence_unitIso : commGroupAddCommGroupEquivalence.unitIso = CategoryTheory.Iso.refl (CategoryTheory.Functor.id CommGrpCat)
-- Mathlib.CategoryTheory.MorphismProperty.Local
CategoryTheory.MorphismProperty.IsLocalAtTarget.of_le : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C}
  {K L : CategoryTheory.Precoverage C} [P.IsLocalAtTarget L], K ≤ L → P.IsLocalAtTarget K
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.combine' : ℕ → Int.Internal.Linear.Poly → Int.Internal.Linear.Poly → Int.Internal.Linear.Poly
-- Mathlib.Topology.Separation.Hausdorff
t2_separation_nhds : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T2Space X] {x y : X},
  x ≠ y → ∃ u v, u ∈ nhds x ∧ v ∈ nhds y ∧ Disjoint u v
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.instBEqExpr.beq : Nat.Internal.Linear.Expr → Nat.Internal.Linear.Expr → Bool
-- Init.Data.SInt.Bitwise
Int32.or_neg_one : ∀ {a : Int32}, a ||| -1 = -1
-- Lean.Data.Lsp.Workspace
Lean.Lsp.FileChangeType.Deleted.sizeOf_spec : sizeOf Lean.Lsp.FileChangeType.Deleted = 1
-- Lean.Meta.ReduceEval
Lean.Meta.ReduceEval.mk : {α : Type} → (Lean.Expr → Lean.MetaM α) → Lean.Meta.ReduceEval α
-- Lean.ScopedEnvExtension
Lean.ScopedEnvExtension.instInhabitedStateStack : {a a_1 a_2 : Type} → Inhabited (Lean.ScopedEnvExtension.StateStack a a_1 a_2)
-- Mathlib.CategoryTheory.GradedObject.Trifunctor
CategoryTheory.GradedObject.instHasMapProdObjFunctorMapTrifunctorObjOfMapTrifunctor : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} C₄]
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄))) {I₁ : Type u_7}
  {I₂ : Type u_8} {I₃ : Type u_9} {J : Type u_10} (p : I₁ × I₂ × I₃ → J) (X₁ : CategoryTheory.GradedObject I₁ C₁)
  (X₂ : CategoryTheory.GradedObject I₂ C₂) (X₃ : CategoryTheory.GradedObject I₃ C₃)
  [h : ((((CategoryTheory.GradedObject.mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p],
  (((CategoryTheory.GradedObject.mapTrifunctorObj F X₁ I₂ I₃).obj X₂).obj X₃).HasMap p
-- Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
/-- For natural numbers `n`, the logarithmic counting function for the poles of `f ^ n` equals `n` times
the logarithmic counting function for the poles of `f`.
 -/
ValueDistribution.logCounting_pow_top : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [inst_1 : ProperSpace 𝕜] {f : 𝕜 → 𝕜} {n : ℕ},
  Meromorphic f → ValueDistribution.logCounting (f ^ n) ⊤ = n • ValueDistribution.logCounting f ⊤
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.Scheme.ofRestrict_appLE : ∀ {U : TopCat} (X : AlgebraicGeometry.Scheme) {f : U ⟶ TopCat.of ↥X}
  (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (V : X.Opens) (W : (X.restrict h).Opens)
  (e : W ≤ (TopologicalSpace.Opens.map (X.ofRestrict h).base).obj V),
  AlgebraicGeometry.Scheme.Hom.appLE (X.ofRestrict h) V W e = X.presheaf.map (CategoryTheory.homOfLE ⋯).op
-- Mathlib.Analysis.Complex.ReImTopology
/-- **Alias** of `Complex.frontier_setOfPred_re_lt`. -/
Complex.frontier_setOf_re_lt : ∀ (a : ℝ), frontier {z | z.re < a} = {z | z.re = a}
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.Monoidal.map_associator'_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.Monoidal] (X Y Z : C) {Z_1 : D}
  (h :
    CategoryTheory.MonoidalCategoryStruct.tensorObj (F.obj X)
        (CategoryTheory.MonoidalCategoryStruct.tensorObj (F.obj Y) (F.obj Z)) ⟶
      Z_1),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).hom h =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Functor.LaxMonoidal.μ F X Y) (F.obj Z))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Functor.LaxMonoidal.μ F (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z)
        (CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom)
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.Functor.OplaxMonoidal.δ F X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z))
            (CategoryTheory.CategoryStruct.comp
              (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj X)
                (CategoryTheory.Functor.OplaxMonoidal.δ F Y Z))
              h))))
-- Mathlib.Order.SuccPred.Limit
Order.IsPredPrelimit.isGLB_Ioi : ∀ {α : Type u_1} {a : α} [inst : LinearOrder α], Order.IsPredPrelimit a → IsGLB (Set.Ioi a) a
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
CategoryTheory.Bicategory.RightAdjoint.mk.injEq : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {a b : B} {left : a ⟶ b} (right : b ⟶ a)
  (adj : CategoryTheory.Bicategory.Adjunction left right) (right_1 : b ⟶ a)
  (adj_1 : CategoryTheory.Bicategory.Adjunction left right_1),
  ({ right := right, adj := adj } = { right := right_1, adj := adj_1 }) = (right = right_1 ∧ adj ≍ adj_1)
-- Mathlib.Data.Rel
/-- A relation `R` on a type `α` is well-founded if all elements of `α` are accessible within `R`.
 -/
SetRel.IsWellFounded : {α : Type u_1} → SetRel α α → Prop
-- Lean.PrettyPrinter.Parenthesizer
Lean.PrettyPrinter.Parenthesizer.eoi.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Topology.Convenient.OpenClosed
IsOpen.isGeneratedBy : ∀ {ι : Type u_1} {X : ι → Type u_2} [inst : (i : ι) → TopologicalSpace (X i)] {Y : Type u_3}
  [inst_1 : TopologicalSpace Y] [∀ (i : ι) (U : TopologicalSpace.Opens (X i)), Topology.IsGeneratedBy X ↥U]
  [Topology.IsGeneratedBy X Y] {U : Set Y}, IsOpen U → Topology.IsGeneratedBy X ↑U
-- Mathlib.Data.PFunctor.Univariate.M
PFunctor.Approx.Agree.below.continu : ∀ {F : PFunctor.{uA, uB}}
  {motive :
    {n : ℕ} →
      (a : PFunctor.Approx.CofixA F n) → (a_1 : PFunctor.Approx.CofixA F (n + 1)) → PFunctor.Approx.Agree a a_1 → Prop}
  (x : PFunctor.Approx.CofixA F 0) (y : PFunctor.Approx.CofixA F 1), PFunctor.Approx.Agree.below ⋯
-- Mathlib.Data.Finset.Powerset
Finset.powerset_inj : ∀ {α : Type u_1} {s t : Finset α}, s.powerset = t.powerset ↔ s = t
-- Mathlib.GroupTheory.Index
/-- Relative version of `Subgroup.index_dvd_two_iff'`.  -/
Subgroup.relIindex_dvd_two_iff' : ∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G}, H.relIndex K ∣ 2 ↔ ∃ a ∈ K, ∀ b ∈ K, a * b ∈ H ∨ b ∈ H
-- Mathlib.RingTheory.Multiplicity
Int.emultiplicity_natAbs : ∀ (a : ℕ) (b : ℤ), emultiplicity a b.natAbs = emultiplicity (↑a) b
-- Mathlib.Tactic.ITauto
/-- Map a function over the proof (regardless of whether the proof is successful or not).  -/
Mathlib.Tactic.ITauto.mapProof : (Mathlib.Tactic.ITauto.Proof → Mathlib.Tactic.ITauto.Proof) →
  Bool × Mathlib.Tactic.ITauto.Proof → Bool × Mathlib.Tactic.ITauto.Proof
-- Lean.Compiler.Specialize
Lean.Compiler.hasSpecializeAttribute : Lean.Environment → Lean.Name → Bool
-- Mathlib.Algebra.Module.FinitePresentation
Module.FinitePresentation.exists_fin : ∀ (R : Type u) (M : Type u_1) [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [fp : Module.FinitePresentation R M], ∃ n K x, K.FG
-- Mathlib.Data.List.Cycle
_private.Mathlib.Data.List.Cycle.0.Cycle.decidableNontrivialCoe.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α → Sort u_2) (h_1 : Unit → motive []) (h_2 : (x : α) → motive [x])
  (h_3 : (x y : α) → (l : List α) → motive (x :: y :: l)),
  (match [] with
    | [] => h_1 ()
    | [x] => h_2 x
    | x :: y :: l => h_3 x y l) =
    h_1 ()
-- Mathlib.Analysis.InnerProductSpace.PiL2
/-- The inner product of a row of `A` and a row of `B` is an entry of `B * Aᴴ`.  -/
inner_matrix_row_row : ∀ {𝕜 : Type u_3} [inst : RCLike 𝕜] {m : Type u_7} {n : Type u_8} [inst_1 : Fintype n] (A B : Matrix m n 𝕜) (i j : m),
  inner 𝕜 (WithLp.toLp 2 (A i)) (WithLp.toLp 2 (B j)) = (B * A.conjTranspose) j i
-- Mathlib.Logic.Equiv.Basic
Equiv.arrowCongr.eq_1 : ∀ {α₁ : Sort u_1} {β₁ : Sort u_2} {α₂ : Sort u_3} {β₂ : Sort u_4} (e₁ : α₁ ≃ α₂) (e₂ : β₁ ≃ β₂),
  e₁.arrowCongr e₂ =
    { toFun := fun f => ⇑e₂ ∘ f ∘ ⇑e₁.symm, invFun := fun f => ⇑e₂.symm ∘ f ∘ ⇑e₁, left_inv := ⋯, right_inv := ⋯ }
-- Init.Data.Option.Attach
Option.attachWith_some : ∀ {α : Type u_1} {x : α} {P : α → Prop} (h : ∀ (b : α), some x = some b → P b), (some x).attachWith P h = some ⟨x, ⋯⟩
-- Aesop.Frontend.RuleExpr
Lean.Parser.Category.Aesop.rule_expr : Lean.Parser.Category
-- Lean.DocString.Parser
/-- Parses an item from a description list.  -/
Lean.Doc.Parser.descItem : Lean.Doc.Parser.BlockCtxt → Lean.Parser.ParserFn
-- Mathlib.Algebra.Order.Monoid.Unbundled.Pow
instIsAddTorsionFreeOfAddLeftStrictMonoOfAddRightStrictMono : ∀ {M : Type u_3} [inst : AddMonoid M] [inst_1 : LinearOrder M] [AddLeftStrictMono M] [AddRightStrictMono M],
  IsAddTorsionFree M
-- Mathlib.CategoryTheory.Sites.Coherent.RegularTopology
/-- Effective epis in a preregular category are stable under composition.  -/
CategoryTheory.regularTopology.instEffectiveEpiComp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preregular C] {X Y Y' : C} (π : Y ⟶ X)
  [CategoryTheory.EffectiveEpi π] (π' : Y' ⟶ Y) [CategoryTheory.EffectiveEpi π'],
  CategoryTheory.EffectiveEpi (CategoryTheory.CategoryStruct.comp π' π)
-- Mathlib.Combinatorics.SimpleGraph.Dart
SimpleGraph.Dart.toProd_injective : ∀ {V : Type u_1} {G : SimpleGraph V}, Function.Injective SimpleGraph.Dart.toProd
-- Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
Profinite.NobelingProof.GoodProducts.range_equiv_factorization : ∀ {I : Type u} (C : Set (I → Bool)) [inst : LinearOrder I] [inst_1 : WellFoundedLT I] {o : Ordinal.{u}}
  (ho : Order.IsSuccLimit o) (hsC : Profinite.NobelingProof.contained C o),
  (fun p => ↑p) ∘ (Profinite.NobelingProof.GoodProducts.range_equiv C ho hsC).toFun = fun p => ↑p
-- Mathlib.RingTheory.Polynomial.IntegralNormalization
Polynomial.integralNormalization_eval₂_leadingCoeff_mul : ∀ {R : Type u} {S : Type v} [inst : Semiring R] {p : Polynomial R} [inst_1 : CommSemiring S],
  1 ≤ p.natDegree →
    ∀ (f : R →+* S) (x : S),
      Polynomial.eval₂ f (f p.leadingCoeff * x) p.integralNormalization =
        f p.leadingCoeff ^ (p.natDegree - 1) * Polynomial.eval₂ f x p
-- Mathlib.Data.Prod.Basic
Prod.snd_eq_iff : ∀ {α : Type u_1} {β : Type u_2} {p : α × β} {x : β}, p.2 = x ↔ p = (p.1, x)
-- Mathlib.Analysis.Normed.Ring.Lemmas
Dilation.mulRight_toFun : ∀ {α : Type u_1} [inst : NonUnitalNormedRing α] [inst_1 : NormMulClass α] (a : α) (ha : a ≠ 0) (b : α),
  (Dilation.mulRight a ha) b = b * a
-- Std.Data.TreeMap.Iterator
Std.TreeMap.toList.eq_1 : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t : Std.TreeMap α β cmp),
  t.toList = Std.DTreeMap.Const.toList t.inner
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
MultilinearMap.constOfIsEmpty.congr_simp : ∀ (R : Type uR) {ι : Type uι} (M₁ : ι → Type v₁) {M₂ : Type v₂} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
  [inst_4 : Module R M₂] [inst_5 : IsEmpty ι] (m m_1 : M₂),
  m = m_1 → MultilinearMap.constOfIsEmpty R M₁ m = MultilinearMap.constOfIsEmpty R M₁ m_1
-- Mathlib.Data.Set.Insert
Set.mem_singleton : ∀ {α : Type u_1} (a : α), a ∈ {a}
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
/-- If two ring homomorphisms from `SkewMonoidAlgebra k G` are equal on all `single a 1`
and `single 1 b`, then they are equal.  -/
SkewMonoidAlgebra.ringHom_ext : ∀ {k : Type u_1} {G : Type u_2} [inst : Semiring k] [inst_1 : Monoid G] [inst_2 : MulSemiringAction G k]
  {f g : SkewMonoidAlgebra k G →+* k},
  (∀ (b : k), f (SkewMonoidAlgebra.single 1 b) = g (SkewMonoidAlgebra.single 1 b)) →
    (∀ (a : G), f (SkewMonoidAlgebra.single a 1) = g (SkewMonoidAlgebra.single a 1)) → f = g
-- Mathlib.Data.NNRat.Defs
/-- Reinterpret a rational number `q` as a non-negative rational number. Returns `0` if `q ≤ 0`.  -/
Rat.toNNRat : ℚ → ℚ≥0
-- Mathlib.NumberTheory.Padics.PadicVal.Basic
padicValInt_mul_eq_succ : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] (a : ℤ), a ≠ 0 → padicValInt p (a * ↑p) = padicValInt p a + 1
-- Mathlib.Topology.EMetricSpace.Pi
edist_pi_const : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : Fintype β] [Nonempty β] (a b : α),
  (edist (fun x => a) fun x => b) = edist a b
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.NonemptyCompacts.instMax : {α : Type u_1} → [inst : TopologicalSpace α] → Max (TopologicalSpace.NonemptyCompacts α)
-- Mathlib.LinearAlgebra.Basis.Basic
Module.Basis.mem_span_image : ∀ {ι : Type u_1} {R : Type u_3} {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (b : Module.Basis ι R M) {m : M} {s : Set ι}, m ∈ Submodule.span R (⇑b '' s) ↔ ↑(b.repr m).support ⊆ s
-- Mathlib.Analysis.Complex.Trigonometric
Complex.cot_eq_cos_div_sin : ∀ (x : ℂ), x.cot = Complex.cos x / Complex.sin x
-- Mathlib.CategoryTheory.Preadditive.Schur
CategoryTheory.finrank_hom_simple_simple_eq_zero_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] (𝕜 : Type u_2)
  [inst_2 : Field 𝕜] [IsAlgClosed 𝕜] [inst_4 : CategoryTheory.Linear 𝕜 C] [CategoryTheory.Limits.HasKernels C] (X Y : C)
  [FiniteDimensional 𝕜 (X ⟶ X)] [FiniteDimensional 𝕜 (X ⟶ Y)] [CategoryTheory.Simple X] [CategoryTheory.Simple Y],
  Module.finrank 𝕜 (X ⟶ Y) = 0 ↔ IsEmpty (X ≅ Y)
-- Std.Do.PostCond
Std.Do.ExceptConds.const.eq_2 : ∀ (p : Prop) (σ : Type u) (s : Std.Do.PostShape), Std.Do.ExceptConds.const p = Std.Do.ExceptConds.const p
-- Mathlib.CategoryTheory.Monoidal.Hopf_
/-- A Hopf monoid in a braided category `C` is a bimonoid object in `C` equipped with an antipode.
 -/
CategoryTheory.Hopf : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] → [CategoryTheory.BraidedCategory C] → Type (max u₁ v₁)
-- Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.Datatypes
/-- `Tableau` is a structure the Simplex Algorithm operates on. The `i`-th row of `mat` expresses the
variable `basic[i]` as a linear combination of variables from `free`.
 -/
Mathlib.Tactic.Linarith.SimplexAlgorithm.Tableau : (matType : ℕ → ℕ → Type) → [Mathlib.Tactic.Linarith.SimplexAlgorithm.UsableInSimplexAlgorithm matType] → Type
-- Mathlib.Topology.MetricSpace.Antilipschitz
AntilipschitzWith.edist_ne_top : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoEMetricSpace α] [inst_1 : PseudoMetricSpace β] {K : NNReal} {f : α → β},
  AntilipschitzWith K f → ∀ (x y : α), edist x y ≠ ⊤
-- Mathlib.CategoryTheory.Localization.Triangulated
CategoryTheory.Triangulated.Localization.isTriangulated_functor : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (L : CategoryTheory.Functor C D)
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : CategoryTheory.Limits.HasZeroObject C] [inst_5 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [inst_6 : CategoryTheory.Pretriangulated C] [inst_7 : CategoryTheory.HasShift D ℤ] [inst_8 : L.CommShift ℤ]
  (W : CategoryTheory.MorphismProperty C) [inst_9 : L.IsLocalization W] [inst_10 : W.HasLeftCalculusOfFractions]
  [inst_11 : W.IsCompatibleWithTriangulation] [inst_12 : CategoryTheory.Limits.HasZeroObject D]
  [inst_13 : CategoryTheory.Preadditive D] [inst_14 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive]
  [inst_15 : L.Additive], L.IsTriangulated
-- Mathlib.MeasureTheory.Group.Prod
MeasureTheory.measure_inv_null : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Group G] [MeasurableMul₂ G] (μ : MeasureTheory.Measure G)
  [MeasureTheory.SFinite μ] {s : Set G} [MeasurableInv G] [μ.IsMulLeftInvariant], μ s⁻¹ = 0 ↔ μ s = 0
-- Batteries.Tactic.Lint.Basic
Batteries.Tactic.Lint.NamedLinter.mk : Batteries.Tactic.Lint.Linter → Lean.Name → Lean.Name → Batteries.Tactic.Lint.NamedLinter
-- Mathlib.Topology.Algebra.PontryaginDual
/-- A discrete monoid has compact Pontryagin dual.  -/
instLocallyCompactSpacePontryaginDual : ∀ (H : Type u_5) [inst : Group H] [inst_1 : TopologicalSpace H] [IsTopologicalGroup H] [LocallyCompactSpace H],
  LocallyCompactSpace (PontryaginDual H)
-- Mathlib.Data.Quot
/-- Weaken the relation of a quotient. This is the same as `Quot.map id`.  -/
Quot.factor : {α : Type u_4} → (r s : α → α → Prop) → (∀ (x y : α), r x y → s x y) → Quot r → Quot s
-- Std.Data.DTreeMap.Internal.Queries
/-- Returns the value for the key `k`.  -/
Std.DTreeMap.Internal.Impl.Const.get : {α : Type u} →
  {δ : Type w} →
    [inst : Ord α] →
      (t : Std.DTreeMap.Internal.Impl α fun x => δ) → (k : α) → Std.DTreeMap.Internal.Impl.contains k t = true → δ
-- Mathlib.Algebra.Polynomial.Eval.Coeff
Polynomial.map_id : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, Polynomial.map (RingHom.id R) p = p
-- Mathlib.Tactic.FunProp.Types
/-- Simp's cache is used as the `fun_prop` tactic is designed to be used inside of simp and
utilize its cache. It holds successful goals.  -/
Mathlib.Meta.FunProp.State.cache : Mathlib.Meta.FunProp.State → Lean.Meta.Simp.Cache
-- Lean.Parser.Tactic.Doc
/-- Enumerate the tactic tags that are available  -/
Lean.Parser.Tactic.Doc.allTags : {m : Type → Type} → [Monad m] → [Lean.MonadEnv m] → m (List Lean.Name)
-- Mathlib.Tactic.Algebraize
Mathlib.Tactic.Algebraize.Config.mk.injEq : ∀ (properties properties_1 : Bool),
  ({ properties := properties } = { properties := properties_1 }) = (properties = properties_1)
-- Mathlib.Analysis.BoxIntegral.Partition.Tagged
BoxIntegral.TaggedPrepartition.single.congr_simp : ∀ {ι : Type u_1} (I J J_1 : BoxIntegral.Box ι) (e_J : J = J_1) (hJ : J ≤ I) (x x_1 : ι → ℝ) (e_x : x = x_1)
  (h : x ∈ BoxIntegral.Box.Icc I),
  BoxIntegral.TaggedPrepartition.single I J hJ x h = BoxIntegral.TaggedPrepartition.single I J_1 ⋯ x_1 ⋯
-- Mathlib.Analysis.Convex.Cone.Basic
ProperCone.smul_mem : ∀ {R : Type u_2} {E : Type u_3} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommMonoid E] [inst_4 : TopologicalSpace E] [inst_5 : Module R E] {r : R} {x : E} (C : ProperCone R E),
  x ∈ C → 0 ≤ r → r • x ∈ C
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
NumberField.mixedEmbedding.fundamentalCone.integerSetTorsionSMul_stabilizer : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K]
  (a : ↑(NumberField.mixedEmbedding.fundamentalCone.integerSet K)),
  MulAction.stabilizer (↥(NumberField.Units.torsion K)) a = ⊥
-- Lean.Environment
_private.Lean.Environment.0.Lean.EnvExtension.mk.inj : ∀ {σ : Type} {idx : ℕ} {mkInitial : IO σ} {asyncMode : Lean.EnvExtension.AsyncMode} {replay? : Option (Lean.ReplayFn σ)}
  {idx_1 : ℕ} {mkInitial_1 : IO σ} {asyncMode_1 : Lean.EnvExtension.AsyncMode} {replay?_1 : Option (Lean.ReplayFn σ)},
  { idx := idx, mkInitial := mkInitial, asyncMode := asyncMode, replay? := replay? } =
      { idx := idx_1, mkInitial := mkInitial_1, asyncMode := asyncMode_1, replay? := replay?_1 } →
    idx = idx_1 ∧ mkInitial = mkInitial_1 ∧ asyncMode = asyncMode_1 ∧ replay? = replay?_1
-- Init.Data.String.Lemmas.Pattern.String.Basic
String.Slice.Pattern.Model.ForwardStringSearcher.isLongestMatchAtChain_iff_isLongestMatchAtChain_toSlice : ∀ {pat : String} {s : String.Slice} {pos₁ pos₂ : s.Pos},
  String.Slice.Pattern.Model.IsLongestMatchAtChain pat pos₁ pos₂ ↔
    String.Slice.Pattern.Model.IsLongestMatchAtChain pat.toSlice pos₁ pos₂
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.mop_tensorHom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {X₁ Y₁ X₂ Y₂ : C} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂),
  (CategoryTheory.MonoidalCategoryStruct.tensorHom f g).mop =
    CategoryTheory.MonoidalCategoryStruct.tensorHom g.mop f.mop
-- Mathlib.Algebra.Star.Module
star_inv_intCast_smul : ∀ {R : Type u_1} {M : Type u_2} [inst : DivisionRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : StarAddMonoid M] (n : ℤ) (x : M), star ((↑n)⁻¹ • x) = (↑n)⁻¹ • star x
-- Mathlib.RingTheory.Flat.EquationalCriterion
/-- Every homomorphism from a finitely presented module to a flat module factors through a finite
free module.  -/
Module.Flat.exists_factorization_of_finitePresentation : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [Module.Flat R M]
  {P : Type u_3} [inst_4 : AddCommGroup P] [inst_5 : Module R P] [Module.FinitePresentation R P] (h₁ : P →ₗ[R] M),
  ∃ k h₂ h₃, h₁ = h₃ ∘ₗ h₂
-- Mathlib.NumberTheory.LSeries.Linearity
LSeries_add : ∀ {f g : ℕ → ℂ} {s : ℂ}, LSeriesSummable f s → LSeriesSummable g s → LSeries (f + g) s = LSeries f s + LSeries g s
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegral.integral_ofReal : ∀ {a b : ℝ} {μ : MeasureTheory.Measure ℝ} {f : ℝ → ℝ}, ∫ (x : ℝ) in a..b, ↑(f x) ∂μ = ↑(∫ (x : ℝ) in a..b, f x ∂μ)
-- Init.Data.Order.MinMaxOn
maxOn.congr_simp : ∀ {β : Type u_1} {α : Sort u_2} [i : LE β] {inst : DecidableLE β} [inst_1 : DecidableLE β] (f f_1 : α → β),
  f = f_1 → ∀ (x x_1 : α), x = x_1 → ∀ (y y_1 : α), y = y_1 → maxOn f x y = maxOn f_1 x_1 y_1
-- Mathlib.Analysis.Normed.Module.RCLike.Real
/-- If `E` is a nontrivial topological module over `ℝ`, then `E` has no isolated points.
This is a particular case of `Module.punctured_nhds_neBot`.  -/
Real.punctured_nhds_module_neBot : ∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : TopologicalSpace E] [ContinuousAdd E] [Nontrivial E]
  [inst_4 : Module ℝ E] [ContinuousSMul ℝ E] (x : E), (nhdsWithin x {x}ᶜ).NeBot
-- Mathlib.Algebra.Polynomial.Derivative
Polynomial.pow_sub_dvd_iterate_derivative_of_pow_dvd : ∀ {R : Type u} [inst : CommSemiring R] {p q : Polynomial R} {n : ℕ} (m : ℕ),
  q ^ n ∣ p → q ^ (n - m) ∣ (⇑Polynomial.derivative)^[m] p
-- Mathlib.Order.RelSeries
SetRel.FiniteDimensional.inv : ∀ {α : Type u_1} (r : SetRel α α) [r.FiniteDimensional], r.inv.FiniteDimensional
-- Mathlib.Data.List.NodupEquivFin
List.Nodup.getBijectionOfForallMemList_coe : ∀ {α : Type u_1} (l : List α) (nd : l.Nodup) (h : ∀ (x : α), x ∈ l) (i : Fin l.length),
  ↑(List.Nodup.getBijectionOfForallMemList l nd h) i = l.get i
-- Aesop.Builder.Basic
Aesop.PhaseSpec.unsafe.injEq : ∀ (info info_1 : Aesop.UnsafeRuleInfo), (Aesop.PhaseSpec.unsafe info = Aesop.PhaseSpec.unsafe info_1) = (info = info_1)
-- Mathlib.AlgebraicTopology.ModelCategory.Homotopy
HomotopicalAlgebra.LeftHomotopyRel.rightHomotopyRel : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C] {X Y : C}
  {f g : X ⟶ Y} [HomotopicalAlgebra.IsCofibrant X],
  HomotopicalAlgebra.LeftHomotopyRel f g → HomotopicalAlgebra.RightHomotopyRel f g
-- Mathlib.Order.Max
IsBot.lt_of_ne' : ∀ {α : Type u_1} [inst : PartialOrder α] {a b : α}, IsBot a → b ≠ a → a < b
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.sin_eq_sqrt_one_sub_cos_sq : ∀ {x : ℝ}, 0 ≤ x → x ≤ Real.pi → Real.sin x = √(1 - Real.cos x ^ 2)
-- Mathlib.Topology.OpenPartialHomeomorph.Defs
/-- **Alias** of `OpenPartialHomeomorph.coe_toPartialEquiv`. -/
OpenPartialHomeomorph.coe_coe : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y), ↑e.toPartialEquiv = ↑e