mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Triangulated.Subcategory
CategoryTheory.ObjectProperty.instIsTriangulatedEssImageOfIsTriangulatedOfFull : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  {D : Type u_2} [inst_6 : CategoryTheory.Category.{v_2, u_2} D] [inst_7 : CategoryTheory.Preadditive D]
  [inst_8 : CategoryTheory.Limits.HasZeroObject D] [inst_9 : CategoryTheory.HasShift D ℤ]
  [inst_10 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [inst_11 : CategoryTheory.Pretriangulated D]
  (F : CategoryTheory.Functor C D) [inst_12 : F.CommShift ℤ] [F.IsTriangulated] [F.Full], F.essImage.IsTriangulated
-- Mathlib.Analysis.Normed.Group.Quotient
/-- The quotient in the category of normed groups.  -/
QuotientAddGroup.instNormedAddCommGroup : {M : Type u_1} →
  [inst : SeminormedAddCommGroup M] → (S : AddSubgroup M) → [hS : IsClosed ↑S] → NormedAddCommGroup (M ⧸ S)
-- Mathlib.Logic.Relation
Relation.instTransTransGen_mathlib_1 : {α : Type u_1} → {r : α → α → Prop} → Trans r (Relation.TransGen r) (Relation.TransGen r)
-- Init.Grind.ToInt
Lean.Grind.instInhabitedIntInterval.default : Lean.Grind.IntInterval
-- Init.Data.UInt.Bitwise
UInt32.shiftLeft_xor : ∀ {a b c : UInt32}, (a ^^^ b) <<< c = a <<< c ^^^ b <<< c
-- Batteries.Data.List.Lemmas
List.idxOfNth_lt_length_iff : ∀ {α : Type u_1} {x : α} {n : ℕ} [inst : BEq α] {xs : List α}, List.idxOfNth x xs n < xs.length ↔ n < List.count x xs
-- Lean.Parser.Module.Syntax
Lean.Parser.Module.public.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Analysis.Calculus.ContDiffHolder.Pointwise
/-- If `f` is a $C^{k+(α)}$ function and `l + m ≤ k`, then $D^mf$ is a $C^{l + (α)}$ function.  -/
ContDiffPointwiseHolderAt.iteratedFDeriv : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] {k l m : ℕ} {α : ↑unitInterval} {f : E → F} {a : E},
  ContDiffPointwiseHolderAt k α f a → l + m ≤ k → ContDiffPointwiseHolderAt l α (iteratedFDeriv ℝ m f) a
-- Mathlib.RingTheory.LocalRing.MaximalIdeal.Square
/-- In a Noetherian local ring of positive Krull dimension,
the square of the maximal ideal is strictly contained in the maximal ideal.  -/
IsLocalRing.maximalIdeal_sq_lt_of_ringKrullDim_ne_zero : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsLocalRing R] [IsNoetherianRing R],
  ringKrullDim R ≠ 0 → IsLocalRing.maximalIdeal R ^ 2 < IsLocalRing.maximalIdeal R
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic
_private.Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic.0.CategoryTheory.WithInitial.opEquiv.match_3.splitter : (C : Type u_1) →
  [inst : CategoryTheory.Category.{u_2, u_1} C] →
    (motive : (x y : (CategoryTheory.WithInitial C)ᵒᵖ) → (Opposite.unop y ⟶ Opposite.unop x) → (x ⟶ y) → Sort u_3) →
      (x y : (CategoryTheory.WithInitial C)ᵒᵖ) →
        (f : Opposite.unop y ⟶ Opposite.unop x) →
          (x_1 : x ⟶ y) →
            ((x y : C) →
                (f :
                    Opposite.unop (Opposite.op (CategoryTheory.WithInitial.of y)) ⟶
                      Opposite.unop (Opposite.op (CategoryTheory.WithInitial.of x))) →
                  (x_2 :
                      Opposite.op (CategoryTheory.WithInitial.of x) ⟶ Opposite.op (CategoryTheory.WithInitial.of y)) →
                    motive (Opposite.op (CategoryTheory.WithInitial.of x))
                      (Opposite.op (CategoryTheory.WithInitial.of y)) f x_2) →
              ((a : C) →
                  (x :
                      Opposite.unop (Opposite.op CategoryTheory.WithInitial.star) ⟶
                        Opposite.unop (Opposite.op (CategoryTheory.WithInitial.of a))) →
                    (x_2 :
                        Opposite.op (CategoryTheory.WithInitial.of a) ⟶ Opposite.op CategoryTheory.WithInitial.star) →
                      motive (Opposite.op (CategoryTheory.WithInitial.of a))
                        (Opposite.op CategoryTheory.WithInitial.star) x x_2) →
                ((x :
                      Opposite.unop (Opposite.op CategoryTheory.WithInitial.star) ⟶
                        Opposite.unop (Opposite.op CategoryTheory.WithInitial.star)) →
                    (x_2 : Opposite.op CategoryTheory.WithInitial.star ⟶ Opposite.op CategoryTheory.WithInitial.star) →
                      motive (Opposite.op CategoryTheory.WithInitial.star) (Opposite.op CategoryTheory.WithInitial.star)
                        x x_2) →
                  motive x y f x_1
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getD_insert_self : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {k : α} {fallback v : β}, (m.insert k v).getD k fallback = v
-- Lean.Parser.Command
Lean.Parser.Command.deriving.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Init.Data.AC
Lean.Data.AC.sort.loop : List ℕ → List ℕ → List ℕ
-- Mathlib.Analysis.Normed.Module.Ball.Pointwise
/-- In a real normed space, the image of the unit ball under scalar multiplication by a positive
constant `r` is the ball of radius `r`.  -/
smul_unitBall_of_pos : ∀ {E : Type u_2} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {r : ℝ},
  0 < r → r • Metric.ball 0 1 = Metric.ball 0 r
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks
CategoryTheory.Limits.PreservesPullback.iso_hom_snd : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst_2 : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) G]
  [inst_3 : CategoryTheory.Limits.HasPullback f g] [inst_4 : CategoryTheory.Limits.HasPullback (G.map f) (G.map g)],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PreservesPullback.iso G f g).hom
      (CategoryTheory.Limits.pullback.snd (G.map f) (G.map g)) =
    G.map (CategoryTheory.Limits.pullback.snd f g)
-- Mathlib.AlgebraicTopology.SimplicialSet.PiZero
SSet.IsConnected.mk : ∀ {X : SSet} [toSubsingleton : Subsingleton X.π₀],
  autoParam X.Nonempty SSet.IsConnected.nonempty._autoParam → X.IsConnected
-- Mathlib.Topology.Order.UpperLowerSetTopology
Topology.instIsUpperSet : ∀ {α : Type u_1} [inst : Preorder α], Topology.IsUpperSet α
-- Aesop.Tree.Data
Aesop.instInhabitedGoalOrigin : Inhabited Aesop.GoalOrigin
-- Mathlib.CategoryTheory.Dialectica.Monoidal
CategoryTheory.Dial.tensorUnitImpl_tgt : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasFiniteProducts C],
  CategoryTheory.Dial.tensorUnitImpl.tgt = ⊤_ C
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getD_empty : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {a : α} {fallback : β}, ∅.getD a fallback = fallback
-- Mathlib.Combinatorics.SimpleGraph.StronglyRegular
SimpleGraph.IsSRGWith.card_commonNeighbors_eq_of_not_adj_compl : ∀ {V : Type u} [inst : Fintype V] {G : SimpleGraph V} [inst_1 : DecidableRel G.Adj] {n k ℓ μ : ℕ}
  [inst_2 : DecidableEq V],
  G.IsSRGWith n k ℓ μ → ∀ {v w : V}, v ≠ w → ¬Gᶜ.Adj v w → Fintype.card ↑(Gᶜ.commonNeighbors v w) = n - (2 * k - ℓ)
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.coe_iInf : ∀ {R : Type u} [inst : NonAssocRing R] {ι : Sort u_1} {S : ι → Subring R}, ↑(⨅ i, S i) = ⋂ i, ↑(S i)
-- Mathlib.Algebra.Homology.Embedding.StupidTrunc
/-- The stupid truncation functor `HomologicalComplex C c' ⥤ HomologicalComplex C c'`
given by an embedding `e : Embedding c c'` of complex shapes.  -/
ComplexShape.Embedding.stupidTruncFunctor : {ι : Type u_1} →
  {ι' : Type u_2} →
    {c : ComplexShape ι} →
      {c' : ComplexShape ι'} →
        (e : c.Embedding c') →
          (C : Type u_3) →
            [inst : CategoryTheory.Category.{v_1, u_3} C] →
              [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
                [CategoryTheory.Limits.HasZeroObject C] →
                  [e.IsRelIff] → CategoryTheory.Functor (HomologicalComplex C c') (HomologicalComplex C c')
-- Mathlib.CategoryTheory.Monoidal.Braided.Multifunctor
/-- The top right map in the reverse hexagon identity.  -/
CategoryTheory.BraidedCategory.ofBifunctor.Reverse.secondMap₁ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      (CategoryTheory.MonoidalCategory.curriedTensor C ≅ (CategoryTheory.MonoidalCategory.curriedTensor C).flip) →
        (CategoryTheory.BraidedCategory.Hexagon.functor₁₂₃' C ⟶ CategoryTheory.BraidedCategory.Hexagon.functor₁₃₂' C)
-- Mathlib.Order.SuccPred.Basic
Order.le_pred_iff_of_not_isMin : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : PredOrder α] {a b : α}, ¬IsMin a → (b ≤ Order.pred a ↔ b < a)
-- Init.Data.List.Attach
List.foldl_pmap : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : List α} {P : α → Prop} {f : (a : α) → P a → β} (H : ∀ a ∈ l, P a)
  (g : γ → β → γ) (x : γ), List.foldl g x (List.pmap f l H) = List.foldl (fun acc a => g acc (f ↑a ⋯)) x l.attach
-- Mathlib.Algebra.Divisibility.Units
isUnit_of_dvd_unit : ∀ {α : Type u_1} [inst : CommMonoid α] {x y : α}, x ∣ y → IsUnit y → IsUnit x
-- Mathlib.CategoryTheory.Generator.Presheaf
CategoryTheory.Presheaf.hasSeparator : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (A : Type u') [inst_1 : CategoryTheory.Category.{v', u'} A]
  [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.HasSeparator A] [CategoryTheory.Limits.HasZeroMorphisms A]
  [CategoryTheory.Limits.HasCoproducts A], CategoryTheory.HasSeparator (CategoryTheory.Functor Cᵒᵖ A)
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Path.Homotopic.Quotient.refl_trans : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x₀ x₁ : X} (γ : Path.Homotopic.Quotient x₀ x₁),
  (Path.Homotopic.Quotient.refl x₀).trans γ = γ
-- Mathlib.Analysis.InnerProductSpace.l2Space
HilbertBasis.repr_self : ∀ {ι : Type u_1} {𝕜 : Type u_2} [inst : RCLike 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : DecidableEq ι] (b : HilbertBasis ι 𝕜 E) (i : ι),
  b.repr (b i) = lp.single 2 i 1
-- Mathlib.Algebra.Module.ZLattice.Basic
instCountable_of_discrete_submodule : ∀ {E : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E] (L : Submodule ℤ E)
  [inst_3 : DiscreteTopology ↥L] [IsZLattice ℝ L], Countable ↥L
-- Mathlib.Data.Finsupp.Defs
Finsupp.zipWith_apply : ∀ {α : Type u_1} {M : Type u_4} {N : Type u_5} {O : Type u_6} [inst : Zero M] [inst_1 : Zero N] [inst_2 : Zero O]
  {f : M → N → O} {hf : f 0 0 = 0} {g₁ : α →₀ M} {g₂ : α →₀ N} {a : α}, (Finsupp.zipWith f hf g₁ g₂) a = f (g₁ a) (g₂ a)
-- Mathlib.Data.Set.Lattice
Set.nonempty_of_nonempty_iUnion_eq_univ : ∀ {α : Type u_1} {ι : Sort u_5} {s : ι → Set α} [Nonempty α], ⋃ i, s i = Set.univ → Nonempty ι
-- Std.Data.ExtDTreeMap.Basic
/-- Inserts multiple elements into the tree map by iterating over the given collection and calling
`insertIfNew`. If the same key appears multiple times, the first occurrence takes precedence.
 -/
Std.ExtDTreeMap.Const.insertManyIfNewUnit : {α : Type u} →
  {cmp : α → α → Ordering} →
    [Std.TransCmp cmp] →
      {ρ : Type u_1} →
        [ForIn Id ρ α] → Std.ExtDTreeMap α (fun x => Unit) cmp → ρ → Std.ExtDTreeMap α (fun x => Unit) cmp
-- Mathlib.Data.Fintype.EquivFin
Equiv.embeddingEquivOfFinite_apply : ∀ (α : Type u_4) [inst : Finite α] (e : α ↪ α), (Equiv.embeddingEquivOfFinite α) e = e.equivOfFiniteSelfEmbedding
-- Mathlib.Algebra.Homology.QuasiIso
quasiIsoAt_iff_comp_right : ∀ {ι : Type u_1} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {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]
  [hφ' : QuasiIsoAt φ' i], QuasiIsoAt (CategoryTheory.CategoryStruct.comp φ φ') i ↔ QuasiIsoAt φ i
-- Mathlib.Data.String.Lemmas
String.IsPrefix.eq_1 : ∀ (x x_1 : String), x.IsPrefix x_1 = (x.toList <+: x_1.toList)
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- A base angle of an isosceles triangle is acute, oriented vector angle form.  -/
Orientation.abs_oangle_sub_left_toReal_lt_pi_div_two : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y : V}, ‖x‖ = ‖y‖ → |(o.oangle (y - x) y).toReal| < Real.pi / 2
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.isEmpty_inter_iff : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashSet.Raw α} [EquivBEq α] [LawfulHashable α],
  m₁.WF → m₂.WF → ((m₁ ∩ m₂).isEmpty = true ↔ ∀ k ∈ m₁, k ∉ m₂)
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd
SSet.prodStdSimplex.pairingCore.IsType₂.simplex_fst_apply : ∀ {m : ℕ} {k : Fin (m + 1)} {n : ℕ} {x : ((SSet.horn (m + 1) k.castSucc).unionProd (SSet.boundary n)).N}
  (hx : SSet.prodStdSimplex.pairingCore.IsType₂ x) {d : ℕ} (hd : x.dim = d) (i : Fin (d + 2)),
  (hx.simplex hd).1 i = (SSet.prodStdSimplex.pairingCore.IsType₂.φ x hd i).1
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousAddEquiv.trans.eq_1 : ∀ {M : Type u_1} {N : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace N] [inst_2 : Add M]
  [inst_3 : Add N] {L : Type u_3} [inst_4 : Add L] [inst_5 : TopologicalSpace L] (cme1 : M ≃ₜ+ N) (cme2 : N ≃ₜ+ L),
  cme1.trans cme2 = { toAddEquiv := cme1.trans cme2.toAddEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }
-- Std.Data.HashMap.Basic
/-- Removes the mapping for the given key if it exists.  -/
Std.HashMap.erase : {α : Type u} → {β : Type v} → {x : BEq α} → {x_1 : Hashable α} → Std.HashMap α β → α → Std.HashMap α β
-- Init.Control.Lawful.Instances
StateT.run_get : ∀ {m : Type u_1 → Type u_2} {σ : Type u_1} [inst : Monad m] (s : σ), get.run s = pure (s, s)
-- Mathlib.Data.Nat.Digits.Defs
/-- Interpreting as a base `p` number and dividing by `p` is the same as interpreting the tail.
 -/
Nat.ofDigits_div_eq_ofDigits_tail : ∀ {p : ℕ}, 0 < p → ∀ (digits : List ℕ), (∀ l ∈ digits, l < p) → Nat.ofDigits p digits / p = Nat.ofDigits p digits.tail
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.isEmpty_insertMany_list : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {l : List (α × β)}, (m.insertMany l).isEmpty = (m.isEmpty && l.isEmpty)
-- Lean.Elab.Do.Basic
Lean.Elab.Do.DoElemContKind.nonDuplicable : Lean.Elab.Do.DoElemContKind
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.get!_inter_of_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  [inst_2 : Inhabited α] {k : α}, k ∈ m₂ → (m₁ ∩ m₂).get! k = m₁.get! k
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Under.postCongr_inv_app_right : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {X : T} {F G : CategoryTheory.Functor T D} (e : F ≅ G) (X_1 : CategoryTheory.Under X),
  ((CategoryTheory.Under.postCongr e).inv.app X_1).right = e.inv.app X_1.right
-- Mathlib.Analysis.Convex.PathConnected
StarConvex.isPathConnected : ∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : Module ℝ E] [inst_2 : TopologicalSpace E] [ContinuousAdd E]
  [ContinuousSMul ℝ E] {s : Set E} {a : E}, StarConvex ℝ a s → a ∈ s → IsPathConnected s
-- Mathlib.Data.List.TFAE
List.TFAE.out : ∀ {l : List Prop},
  l.TFAE →
    ∀ (n₁ n₂ : ℕ) {a b : Prop},
      autoParam (l[n₁]? = some a) List.TFAE.out._auto_1 → autoParam (l[n₂]? = some b) List.TFAE.out._auto_3 → (a ↔ b)
-- Init.Data.Nat.ToString
_private.Init.Data.Nat.ToString.0.Nat.ofDigitChars.eq_1 : ∀ (b : ℕ) (l : List Char) (init : ℕ),
  b.ofDigitChars l init = List.foldl (fun sofar c => b * sofar + (c.toNat - '0'.toNat)) init l
-- Mathlib.CategoryTheory.WithTerminal.Cone
_private.Mathlib.CategoryTheory.WithTerminal.Cone.0.CategoryTheory.WithInitial.coconeLift_obj_ι_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type w} [inst_1 : CategoryTheory.Category.{w', w} J]
  {X : C} {K : CategoryTheory.Functor J (CategoryTheory.Under X)} (t : CategoryTheory.Limits.Cocone K)
  (x : CategoryTheory.WithInitial J),
  (CategoryTheory.WithInitial.coconeLift✝.obj t).ι.app x =
    match x with
    | CategoryTheory.WithInitial.of a => CategoryTheory.Under.Hom.right (t.ι.app a)
    | CategoryTheory.WithInitial.star => t.pt.hom
-- Lean.Compiler.InitAttr
_private.Lean.Compiler.InitAttr.0.Lean.isUnitType : Lean.Expr → Bool
-- Init.Data.Option.Basic
Option.some_get : ∀ {α : Type u_1} {x : Option α} (h : x.isSome = true), some (x.get h) = x
-- Mathlib.MeasureTheory.Measure.Haar.Unique
MeasureTheory.Measure.addHaarScalarFactor_eq_integral_div : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [inst_2 : IsTopologicalAddGroup G]
  [inst_3 : MeasurableSpace G] [inst_4 : BorelSpace G] (μ' μ : MeasureTheory.Measure G) [inst_5 : μ.IsAddHaarMeasure]
  [inst_6 : MeasureTheory.IsFiniteMeasureOnCompacts μ'] [inst_7 : μ'.IsAddLeftInvariant] {f : G → ℝ},
  Continuous f →
    HasCompactSupport f → ∫ (x : G), f x ∂μ ≠ 0 → ↑(μ'.addHaarScalarFactor μ) = (∫ (x : G), f x ∂μ') / ∫ (x : G), f x ∂μ
-- Mathlib.Algebra.CharP.Lemmas
sub_pow_eq_mul_pow_sub_pow_div_expChar_of_commute : ∀ {R : Type u_1} [inst : Ring R] {x y : R} (p n : ℕ) [hR : ExpChar R p],
  Commute x y → (x - y) ^ n = (x - y) ^ (n % p) * (x ^ p - y ^ p) ^ (n / p)
-- Init.Data.UInt.Bitwise
USize.ofBitVec_shiftLeft_mod : ∀ (a : BitVec System.Platform.numBits) (b : ℕ),
  { toBitVec := a <<< (b % System.Platform.numBits) } = { toBitVec := a } <<< USize.ofNat b
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
/-- This is a structure encapsulating the data necessary to define a `Multicospan`.  -/
CategoryTheory.Limits.MulticospanIndex : CategoryTheory.Limits.MulticospanShape →
  (C : Type u) → [CategoryTheory.Category.{v, u} C] → Type (max (max (max u v) w) w')
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.Parser.Aesop.indexing_mode.quot : Lean.ParserDescr
-- Mathlib.CategoryTheory.Triangulated.Pretriangulated
CategoryTheory.Pretriangulated.Triangle.mor₃_eq_zero_iff_epi₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C],
  ∀ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles, T.mor₃ = 0 ↔ CategoryTheory.Epi T.mor₂
-- Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients
Ring.HasFiniteQuotients.cardQuot_pos : ∀ {R : Type u_1} [inst : CommRing R] [Ring.HasFiniteQuotients R] (I : Ideal R), I ≠ ⊥ → 0 < Submodule.cardQuot I
-- Mathlib.Algebra.Module.LinearMap.Defs
LinearMap.ext : ∀ {R : Type u_1} {S : Type u_5} {M : Type u_8} {M₃ : Type u_11} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₃] [inst_4 : Module R M] [inst_5 : Module S M₃] {σ : R →+* S}
  {f g : M →ₛₗ[σ] M₃}, (∀ (x : M), f x = g x) → f = g
-- Mathlib.Algebra.Category.Grp.FilteredColimits
GrpCat.FilteredColimits.colimitCocone.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] [inst_1 : CategoryTheory.IsFiltered J]
  (F : CategoryTheory.Functor J GrpCat),
  GrpCat.FilteredColimits.colimitCocone F =
    { pt := GrpCat.FilteredColimits.colimit F,
      ι :=
        {
          app := fun J_1 =>
            GrpCat.ofHom
              (MonCat.Hom.hom
                ((MonCat.FilteredColimits.colimitCocone (F.comp (CategoryTheory.forget₂ GrpCat MonCat))).ι.app J_1)),
          naturality := ⋯ } }
-- Mathlib.Order.InitialSeg
InitialSeg.inj : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : InitialSeg r s) {a b : α}, f a = f b ↔ a = b
-- Init.Data.UInt.Lemmas
UInt16.zero_mod : ∀ {a : UInt16}, 0 % a = 0
-- Init.Data.Vector.Extract
Vector.extract_reverse : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {i j : ℕ},
  xs.reverse.extract i j = Vector.cast ⋯ (xs.extract (n - j) (n - i)).reverse
-- Mathlib.Data.Set.Functor
Set.fmap_eq_image : ∀ {α β : Type u} {s : Set α} (f : α → β), f <$> s = f '' s
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.IdealSheafData.ext_of_iSup_eq_top : ∀ {X : AlgebraicGeometry.Scheme} {I J : X.IdealSheafData} {ι : Type u_1} (U : ι → ↑X.affineOpens),
  ⨆ i, ↑(U i) = ⊤ → (∀ (i : ι), I.ideal (U i) = J.ideal (U i)) → I = J
-- Mathlib.Algebra.Lie.CartanCriterion
/-- **Cartan's criterion for semisimplicity**: if a finite-dimensional Lie algebra has trivial
solvable radical, then its Killing form is non-degenerate.

See also `LieAlgebra.hasTrivialRadical_iff_isKilling`.  -/
LieAlgebra.HasTrivialRadical.instIsKilling : ∀ (R : Type u_1) (L : Type u_2) [inst : CommRing R] [CharZero R] [IsDomain R] [inst_3 : LieRing L]
  [inst_4 : LieAlgebra R L] [IsNoetherian R L] [Module.Free R L] [LieAlgebra.HasTrivialRadical R L],
  LieAlgebra.IsKilling R L
-- Batteries.Tactic.Lint.Basic
/-- The name of the named linter. This is just the declaration name without the namespace.  -/
Batteries.Tactic.Lint.NamedLinter.name : Batteries.Tactic.Lint.NamedLinter → Lean.Name
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
/-- Any zero object identifies to the kernel of a given monomorphisms.  -/
CategoryTheory.Limits.KernelFork.IsLimit.ofMonoOfIsZero : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y : C} →
        {f : X ⟶ Y} →
          (c : CategoryTheory.Limits.KernelFork f) →
            CategoryTheory.Mono f → CategoryTheory.Limits.IsZero c.pt → CategoryTheory.Limits.IsLimit c
-- Mathlib.Tactic.SplitIfs
/-- A position where a split may apply.
 -/
_private.Mathlib.Tactic.SplitIfs.0.Mathlib.Tactic.SplitPosition : Type
-- Mathlib.Tactic.Linter.DirectoryDependency
/-- `NamePrefixRel` is a datatype for storing relations between name prefixes.

That is, `R : NamePrefixRel` is supposed to answer given names `(n₁, n₂)` whether there are any
prefixes `n₁'` of `n₁` and `n₂'` of `n₂` such that `n₁' R n₂'`.

The current implementation is a `NameMap` of `NameSet`s, testing each prefix of `n₁` and `n₂` in
turn. This can probably be optimized.
 -/
_private.Mathlib.Tactic.Linter.DirectoryDependency.0.Mathlib.Linter.DirectoryDependency.NamePrefixRel : Type
-- Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating
ExteriorAlgebra.liftAlternating_ι_mul : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup N]
  [inst_3 : Module R M] [inst_4 : Module R N] (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (m : M) (x : ExteriorAlgebra R M),
  (ExteriorAlgebra.liftAlternating f) ((ExteriorAlgebra.ι R) m * x) =
    (ExteriorAlgebra.liftAlternating fun i => (f i.succ).curryLeft m) x
-- Mathlib.Analysis.InnerProductSpace.LaxMilgram
InnerProductSpace.continuousLinearMapOfBilin.congr_simp : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : CompleteSpace E] (B B_1 : E →L⋆[𝕜] E →L[𝕜] 𝕜),
  B = B_1 → InnerProductSpace.continuousLinearMapOfBilin B = InnerProductSpace.continuousLinearMapOfBilin B_1
-- Mathlib.Algebra.Group.Equiv.Defs
MulEquiv.symm_bijective : ∀ {M : Type u_4} {N : Type u_5} [inst : Mul M] [inst_1 : Mul N], Function.Bijective MulEquiv.symm
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
/-- Inverse of the `sin` function, returns values in the range `-π / 2 ≤ arcsin x ≤ π / 2`.
It defaults to `-π / 2` on `(-∞, -1)` and to `π / 2` to `(1, ∞)`.  -/
Real.arcsin : ℝ → ℝ
-- Mathlib.Order.Filter.TendstoCofinite
Filter.tendstoCofinite_iff : ∀ {α : Type u_1} {β : Type u_2} (f : α → β), Filter.TendstoCofinite f ↔ Filter.Tendsto f Filter.cofinite Filter.cofinite