mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.Module.Defs
smul_lt_smul' : ∀ {α : Type u_1} {β : Type u_2} {a₁ a₂ : α} {b₁ b₂ : β} [inst : SMul α β] [inst_1 : Preorder α] [inst_2 : Preorder β]
  [inst_3 : Zero α] [inst_4 : Zero β] [PosSMulStrictMono α β] [SMulPosStrictMono α β],
  a₁ < a₂ → b₁ < b₂ → 0 < a₂ → 0 < b₁ → a₁ • b₁ < a₂ • b₂
-- Mathlib.Order.Cover
Pi.wcovBy_iff_exists_right_eq : ∀ {ι : Type u_3} {α : ι → Type u_4} [inst : (i : ι) → PartialOrder (α i)] {a b : (i : ι) → α i} [Nonempty ι]
  [inst_2 : DecidableEq ι], a ⩿ b ↔ ∃ i x, a i ⩿ x ∧ b = Function.update a i x
-- Mathlib.LinearAlgebra.Determinant
Module.Basis.det_reindex : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {ι : Type u_4}
  [inst_3 : DecidableEq ι] [inst_4 : Fintype ι] {ι' : Type u_6} [inst_5 : Fintype ι'] [inst_6 : DecidableEq ι']
  (b : Module.Basis ι R M) (v : ι' → M) (e : ι ≃ ι'), (b.reindex e).det v = b.det (v ∘ ⇑e)
-- Mathlib.RepresentationTheory.Homological.FiniteCyclic
/-- Given a finite cyclic group `G` generated by `g : G`, let `P` denote the periodic chain complex
of `k`-linear `G`-representations given by
`... ⟶ k[G] --N--> k[G] --(ρ(g) - 𝟙)--> k[G] --N--> k[G] --(ρ(g) - 𝟙)--> k[G] ⟶ 0` where `ρ` is
the left regular representation and `N` is the norm map. This is the chain morphism from `P` to
the chain complex concentrated at 0 by the trivial representation `k` used to show `P` is a
projective resolution of `k`. It sends `x : k[G]` to the sum of its coefficients.  -/
Rep.FiniteCyclicGroup.resolution.π : (k : Type u) →
  {G : Type u} →
    [inst : CommRing k] →
      [inst_1 : CommGroup G] →
        [inst_2 : Fintype G] →
          (g : G) →
            (Rep.FiniteCyclicGroup.chainComplexFunctor k g).obj (Rep.leftRegular k G) ⟶
              (ChainComplex.single₀ (Rep.{u, u, u} k G)).obj (Rep.trivial k G k)
-- Mathlib.Analysis.Meromorphic.Basic
/-- Eta-expanded form of `Meromorphic.pow` -/
Meromorphic.fun_pow : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {f : 𝕜 → 𝕜'} {n : ℕ}, Meromorphic f → Meromorphic fun i => f i ^ n
-- Mathlib.Analysis.Calculus.ContDiff.Defs
_private.Mathlib.Analysis.Calculus.ContDiff.Defs.0.ContDiffWithinAt.match_1.splitter : (motive : WithTop ℕ∞ → Sort u_1) → (n : WithTop ℕ∞) → (Unit → motive none) → ((n : ℕ∞) → motive (some n)) → motive n
-- Mathlib.Analysis.Calculus.FDeriv.Prod
DifferentiableAt.snd : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {x : E} {f₂ : E → F × G},
  DifferentiableAt 𝕜 f₂ x → DifferentiableAt 𝕜 (fun x => (f₂ x).2) x
-- Lean.Meta.Tactic.Grind.CheckResult
Lean.Meta.Grind.CheckResult.none.sizeOf_spec : sizeOf Lean.Meta.Grind.CheckResult.none = 1
-- Mathlib.Algebra.Group.Action.Basic
/-- When `M` is a monoid, `ArrowAction` is additionally a `MulDistribMulAction`.  -/
arrowMulDistribMulAction : {M : Type u_2} →
  {G : Type u_7} →
    {A : Type u_8} → [inst : DivisionMonoid G] → [MulAction G A] → [inst_2 : Monoid M] → MulDistribMulAction G (A → M)
-- Mathlib.Algebra.BigOperators.Fin
Fin.prod_Ico_cast : ∀ {M : Type u_2} [inst : CommMonoid M] {n m : ℕ} (h : n = m) (f : Fin m → M) (a b : Fin n),
  ∏ i ∈ Finset.Ico (Fin.cast h a) (Fin.cast h b), f i = ∏ i ∈ Finset.Ico a b, f (Fin.cast h i)
-- Mathlib.GroupTheory.GroupAction.Primitive
AddAction.IsPreprimitive.of_surjective : ∀ {M : Type u_3} [inst : AddGroup M] {α : Type u_4} [inst_1 : AddAction M α] {N : Type u_5} {β : Type u_6}
  [inst_2 : AddGroup N] [inst_3 : AddAction N β] {φ : M → N} {f : α →ₑ[φ] β} [AddAction.IsPreprimitive M α],
  Function.Surjective ⇑f → AddAction.IsPreprimitive N β
-- Mathlib.Logic.Basic
eq_cast_iff_heq : ∀ {α β : Sort u} {e : β = α} {a : α} {b : β}, a = cast e b ↔ a ≍ b
-- Lean.Elab.Tactic.RCases
/-- This function is used for producing rcases patterns based on a case tree. Suppose that we have
a list of patterns `ps` that will match correctly against the branches of the case tree for one
constructor. This function will merge tuples at the end of the list, so that `[a, b, ⟨c, d⟩]`
becomes `⟨a, b, c, d⟩` instead of `⟨a, b, ⟨c, d⟩⟩`.

We must be careful to turn `[a, ⟨⟩]` into `⟨a, ⟨⟩⟩` instead of `⟨a⟩` (which will not perform the
nested match).
 -/
_private.Lean.Elab.Tactic.RCases.0.Lean.Elab.Tactic.RCases.RCasesPatt.tuple₁Core : List Lean.Elab.Tactic.RCases.RCasesPatt → List Lean.Elab.Tactic.RCases.RCasesPatt
-- Init.Data.Array.Lemmas
List.foldl_push_eq_append : ∀ {α : Type u_1} {β : Type u_2} {l : List α} {f : α → β} {xs : Array β},
  List.foldl (fun xs x => xs.push (f x)) xs l = xs ++ (List.map f l).toArray
-- Init.Data.SInt.Lemmas
UInt64.toUInt64_toInt64 : ∀ (x : UInt64), x.toInt64.toUInt64 = x
-- Mathlib.Topology.Separation.CompletelyRegular
instCompletelyRegularSpaceSubtype : ∀ {X : Type u} [inst : TopologicalSpace X] {p : X → Prop} [CompletelyRegularSpace X], CompletelyRegularSpace (Subtype p)
-- Lean.Meta.Tactic.Grind.Main
_private.Lean.Meta.Tactic.Grind.Main.0.Lean.Meta.Grind.discharge? : Lean.Expr → Lean.Meta.SimpM (Option Lean.Expr)
-- Mathlib.Data.ENat.Basic
ENat.map_zero : ∀ {α : Type u_1} (f : ℕ → α), ENat.map f 0 = ↑(f 0)
-- Mathlib.Geometry.Manifold.HasGroupoid
Structomorph.toHomeomorph : {H : Type u} →
  [inst : TopologicalSpace H] →
    {G : StructureGroupoid H} →
      {M : Type u_5} →
        {M' : Type u_6} →
          [inst_1 : TopologicalSpace M] →
            [inst_2 : TopologicalSpace M'] →
              [inst_3 : ChartedSpace H M] → [inst_4 : ChartedSpace H M'] → Structomorph G M M' → M ≃ₜ M'
-- Mathlib.Topology.Instances.Matrix
HasSum.matrix_blockDiag : ∀ {X : Type u_1} {m : Type u_4} {n : Type u_5} {p : Type u_6} {R : Type u_8} [inst : AddCommMonoid R]
  [inst_1 : TopologicalSpace R] {L : SummationFilter X} {f : X → Matrix (m × p) (n × p) R}
  {a : Matrix (m × p) (n × p) R}, HasSum f a L → HasSum (fun x => (f x).blockDiag) a.blockDiag L
-- Mathlib.Order.SymmDiff
bihimp_eq_right : ∀ {α : Type u_2} [inst : BooleanAlgebra α] {a b : α}, bihimp a b = b ↔ a = ⊤
-- Mathlib.Analysis.MeanInequalitiesPow
ENNReal.rpow_add_le_add_rpow : ∀ {p : ℝ} (a b : ENNReal), 0 ≤ p → p ≤ 1 → (a + b) ^ p ≤ a ^ p + b ^ p
-- Mathlib.Algebra.GroupWithZero.Submonoid.Pointwise
AddSubmonoid.mem_inv_pointwise_smul_iff : ∀ {G : Type u_2} {A : Type u_4} [inst : AddMonoid A] [inst_1 : Group G] [inst_2 : DistribMulAction G A] {a : G}
  {S : AddSubmonoid A} {x : A}, x ∈ a⁻¹ • S ↔ a • x ∈ S
-- Init.Grind.ToIntLemmas
Lean.Grind.ToInt.of_lt : ∀ {α : Type u_1} {i : Lean.Grind.IntInterval} [inst : Lean.Grind.ToInt α i] [inst_1 : LT α] [Lean.Grind.ToInt.LT α i]
  {a b : α} {a' b' : ℤ}, ↑a = a' → ↑b = b' → a < b → a' + 1 ≤ b'
-- Init.Data.List.MinMaxIdx
List.maxIdxOn?_singleton : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] {x : α} {f : α → β},
  List.maxIdxOn? f [x] = some 0
-- Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
ModularGroup.coeHom_apply : ∀ (g : Matrix.SpecialLinearGroup (Fin 2) ℤ), ModularGroup.coeHom g = ModularGroup.coe g
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
/-- Mapping from `a : α` (where `ToInt α`) to `toInt a` that has been internalized.
We use this information during model construction.
 -/
Lean.Meta.Grind.Arith.Cutsat.State.toIntVarMap : Lean.Meta.Grind.Arith.Cutsat.State → Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Expr
-- Mathlib.Data.DFinsupp.Sigma
DFinsupp.sigmaCurry_single : ∀ {ι : Type u} {α : ι → Type u_2} {δ : (i : ι) → α i → Type v} [inst : DecidableEq ι]
  [inst_1 : (i : ι) → DecidableEq (α i)] [inst_2 : (i : ι) → (j : α i) → Zero (δ i j)] (ij : (i : ι) × α i)
  (x : δ ij.fst ij.snd), (fun₀ | ij => x).sigmaCurry = fun₀ | ij.fst => fun₀ | ij.snd => x
-- Mathlib.Combinatorics.SimpleGraph.Prod
SimpleGraph.Walk.boxProdLeft.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} (H : SimpleGraph β) {a₁ a₂ : α} (b : β),
  SimpleGraph.Walk.boxProdLeft H b = SimpleGraph.Walk.map (G.boxProdLeft H b).toHom
-- Mathlib.Condensed.Discrete.LocallyConstant
/-- The unit of the adjunction is given by mapping each element to the corresponding constant map.
 -/
CompHausLike.LocallyConstant.unit : (P : TopCat → Prop) →
  [inst : CompHausLike.HasProp P PUnit.{u + 1}] →
    [inst_1 : CompHausLike.HasExplicitFiniteCoproducts P] →
      [inst_2 : CompHausLike.HasExplicitPullbacks P] →
        (hs :
            ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y),
              CategoryTheory.EffectiveEpi f → Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f)) →
          CategoryTheory.Functor.id (Type (max u u_1)) ⟶
            (CompHausLike.LocallyConstant.functor P hs).comp
              ((CategoryTheory.sheafSections (CategoryTheory.coherentTopology (CompHausLike P)) (Type (max u u_1))).obj
                (Opposite.op (CompHausLike.of P PUnit.{u + 1})))
-- Mathlib.Topology.Algebra.InfiniteSum.Ring
Summable.tsum_mul_left : ∀ {ι : Type u_1} {α : Type u_3} {L : SummationFilter ι} [inst : NonUnitalNonAssocSemiring α]
  [inst_1 : TopologicalSpace α] [IsTopologicalSemiring α] {f : ι → α} [T2Space α] [L.NeBot] (a : α),
  Summable f L → ∑'[L] (i : ι), a * f i = a * ∑'[L] (i : ι), f i
-- Mathlib.Analysis.RCLike.Basic
RCLike.ofReal_finsuppProd : ∀ {K : Type u_1} [inst : RCLike K] {α : Type u_3} {M : Type u_4} [inst_1 : Zero M] (f : α →₀ M) (g : α → M → ℝ),
  ↑(f.prod fun a b => g a b) = f.prod fun a b => ↑(g a b)
-- Mathlib.Data.Nat.Nth
Nat.count_le_iff_le_nth : ∀ {p : ℕ → Prop} [inst : DecidablePred p], (Set.ofPred p).Infinite → ∀ {a b : ℕ}, Nat.count p a ≤ b ↔ a ≤ Nat.nth p b
-- Mathlib.Algebra.Group.Submonoid.Units
AddSubgroup.addUnitsEquivSelf.eq_1 : ∀ {G : Type u_2} [inst : AddGroup G] (H : AddSubgroup G),
  H.addUnitsEquivSelf = H.addUnitsEquivAddUnitsType.trans toAddUnits.symm
-- Mathlib.Algebra.Polynomial.UnitTrinomial
Polynomial.trinomial_natDegree : ∀ {R : Type u_1} [inst : Semiring R] {k m n : ℕ} {u v w : R},
  k < m → m < n → w ≠ 0 → (Polynomial.trinomial k m n u v w).natDegree = n
-- Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
/-- A morphism of modules that admits a linear retraction induces an injective morphism of
exterior algebras.  -/
ExteriorAlgebra.map_injective : ∀ {R : Type u1} [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {N : Type u4}
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] {f : M →ₗ[R] N},
  (∃ g, g ∘ₗ f = LinearMap.id) → Function.Injective ⇑(ExteriorAlgebra.map f)
-- Mathlib.Analysis.Convex.Between
Wbtw.sameRay_vsub : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : CommRing R] [inst_1 : PartialOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P] {x y z : P},
  Wbtw R x y z → SameRay R (y -ᵥ x) (z -ᵥ y)
-- Mathlib.CategoryTheory.Grothendieck
CategoryTheory.Grothendieck.grothendieckTypeToCat_unitIso_inv_app_fiber : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (G : CategoryTheory.Functor C (Type w))
  (X : CategoryTheory.Grothendieck (G.comp CategoryTheory.typeToCat)),
  ((CategoryTheory.Grothendieck.grothendieckTypeToCat G).unitIso.inv.app X).fiber = CategoryTheory.eqToHom ⋯
-- Mathlib.GroupTheory.GroupAction.Defs
AddAction.instAddAction : {G : Type u_1} → {α : Type u_2} → [inst : AddGroup G] → [AddAction G α] → (H : AddSubgroup G) → AddAction (↥H) α
-- Mathlib.Algebra.Homology.Homotopy
HomotopyEquiv.copy_hom : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {c : ComplexShape ι} {C D : HomologicalComplex V c} (f : HomotopyEquiv C D) {g : C ⟶ D} (h : Homotopy f.hom g),
  (f.copy h).hom = g
-- Mathlib.Algebra.Exact.Basic
/-- The maps `f` and `g` form an exact pair: `g y = 1` iff `y` belongs to the image of `f`.  -/
Function.MulExact : {M : Type u_2} → {N : Type u_4} → {P : Type u_6} → (M → N) → (N → P) → [One P] → Prop
-- Init.Data.Order.Ord
Std.OrientedCmp.lt_of_not_isLE : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.OrientedCmp cmp] {a b : α}, ¬(cmp a b).isLE = true → cmp b a = Ordering.lt
-- Lean.Data.Lsp.Basic
Lean.Lsp.DeleteFile.instToJsonOptions : Lean.ToJson Lean.Lsp.DeleteFile.Options
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey!_inter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  [inst : Inhabited α] {k : α}, (m₁ ∩ m₂).getKey! k = if k ∈ m₂ then m₁.getKey! k else default
-- Mathlib.Algebra.Lie.Derivation.Basic
/-- The set of Lie derivations from a Lie algebra `L` to itself is a Lie algebra.  -/
LieDerivation.instLieAlgebra : {R : Type u_1} →
  {L : Type u_2} →
    [inst : CommRing R] → [inst_1 : LieRing L] → [inst_2 : LieAlgebra R L] → LieAlgebra R (LieDerivation R L L)
-- Mathlib.Algebra.Group.Defs
nsmulRec'_succ : ∀ {M : Type u_2} [inst : Add M] [inst_1 : Zero M] {k : ℕ}, k ≠ 0 → ∀ (m : M), nsmulRec' (k + 1) m = nsmulRec' k m + m
-- Mathlib.AlgebraicTopology.RelativeCellComplex.AttachCells
HomotopicalAlgebra.AttachCells.mk.injEq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {α : Type t} {A B : α → C} {g : (a : α) → A a ⟶ B a}
  {X₁ X₂ : C} {f : X₁ ⟶ X₂} (ι : Type w) (π : ι → α) (cofan₁ : CategoryTheory.Limits.Cofan fun i => A (π i))
  (cofan₂ : CategoryTheory.Limits.Cofan fun i => B (π i)) (isColimit₁ : CategoryTheory.Limits.IsColimit cofan₁)
  (isColimit₂ : CategoryTheory.Limits.IsColimit cofan₂) (m : cofan₁.pt ⟶ cofan₂.pt)
  (hm :
    autoParam
      (∀ (i : ι),
        CategoryTheory.CategoryStruct.comp (cofan₁.inj i) m =
          CategoryTheory.CategoryStruct.comp (g (π i)) (cofan₂.inj i))
      HomotopicalAlgebra.AttachCells.hm._autoParam)
  (g₁ : cofan₁.pt ⟶ X₁) (g₂ : cofan₂.pt ⟶ X₂) (isPushout : CategoryTheory.IsPushout g₁ m f g₂) (ι_1 : Type w)
  (π_1 : ι_1 → α) (cofan₁_1 : CategoryTheory.Limits.Cofan fun i => A (π_1 i))
  (cofan₂_1 : CategoryTheory.Limits.Cofan fun i => B (π_1 i)) (isColimit₁_1 : CategoryTheory.Limits.IsColimit cofan₁_1)
  (isColimit₂_1 : CategoryTheory.Limits.IsColimit cofan₂_1) (m_1 : cofan₁_1.pt ⟶ cofan₂_1.pt)
  (hm_1 :
    autoParam
      (∀ (i : ι_1),
        CategoryTheory.CategoryStruct.comp (cofan₁_1.inj i) m_1 =
          CategoryTheory.CategoryStruct.comp (g (π_1 i)) (cofan₂_1.inj i))
      HomotopicalAlgebra.AttachCells.hm._autoParam)
  (g₁_1 : cofan₁_1.pt ⟶ X₁) (g₂_1 : cofan₂_1.pt ⟶ X₂) (isPushout_1 : CategoryTheory.IsPushout g₁_1 m_1 f g₂_1),
  ({ ι := ι, π := π, cofan₁ := cofan₁, cofan₂ := cofan₂, isColimit₁ := isColimit₁, isColimit₂ := isColimit₂, m := m,
        hm := hm, g₁ := g₁, g₂ := g₂, isPushout := isPushout } =
      { ι := ι_1, π := π_1, cofan₁ := cofan₁_1, cofan₂ := cofan₂_1, isColimit₁ := isColimit₁_1,
        isColimit₂ := isColimit₂_1, m := m_1, hm := hm_1, g₁ := g₁_1, g₂ := g₂_1, isPushout := isPushout_1 }) =
    (ι = ι_1 ∧
      π ≍ π_1 ∧
        cofan₁ ≍ cofan₁_1 ∧
          cofan₂ ≍ cofan₂_1 ∧ isColimit₁ ≍ isColimit₁_1 ∧ isColimit₂ ≍ isColimit₂_1 ∧ m ≍ m_1 ∧ g₁ ≍ g₁_1 ∧ g₂ ≍ g₂_1)
-- Mathlib.CategoryTheory.MorphismProperty.Factorization
CategoryTheory.MorphismProperty.MapFactorizationData.mk.injEq : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C} {X Y : C}
  {f : X ⟶ Y} (Z : C) (i : X ⟶ Z) (p : Z ⟶ Y)
  (fac :
    autoParam (CategoryTheory.CategoryStruct.comp i p = f)
      CategoryTheory.MorphismProperty.MapFactorizationData.fac._autoParam)
  (hi : W₁ i) (hp : W₂ p) (Z_1 : C) (i_1 : X ⟶ Z_1) (p_1 : Z_1 ⟶ Y)
  (fac_1 :
    autoParam (CategoryTheory.CategoryStruct.comp i_1 p_1 = f)
      CategoryTheory.MorphismProperty.MapFactorizationData.fac._autoParam)
  (hi_1 : W₁ i_1) (hp_1 : W₂ p_1),
  ({ Z := Z, i := i, p := p, fac := fac, hi := hi, hp := hp } =
      { Z := Z_1, i := i_1, p := p_1, fac := fac_1, hi := hi_1, hp := hp_1 }) =
    (Z = Z_1 ∧ i ≍ i_1 ∧ p ≍ p_1)
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
/-- The opcycles of a homological complex in degree `j` can be computed
by specifying a choice of `c.prev j` and `c.next j`.  -/
HomologicalComplex.homologyIsoSc' : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {ι : Type u_2} →
        {c : ComplexShape ι} →
          (K : HomologicalComplex C c) →
            (i j k : ι) →
              c.prev j = i →
                c.next j = k →
                  [inst_2 : K.HasHomology j] →
                    [inst_3 : (K.sc' i j k).HasHomology] → K.homology j ≅ (K.sc' i j k).homology
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.Measure.instIsHaarMeasureForallVolumeOfMeasurableMulOfSigmaFinite : ∀ {ι : Type u_1} [inst : Fintype ι] {G : ι → Type u_4} [inst_1 : (i : ι) → Group (G i)]
  [inst_2 : (i : ι) → MeasureTheory.MeasureSpace (G i)] [∀ (i : ι), MeasurableMul (G i)]
  [inst_4 : (i : ι) → TopologicalSpace (G i)] [∀ (i : ι), MeasureTheory.SigmaFinite MeasureTheory.volume]
  [∀ (i : ι), MeasureTheory.volume.IsHaarMeasure], MeasureTheory.volume.IsHaarMeasure
-- Mathlib.LinearAlgebra.Matrix.BilinearForm
/-- **Alias** of `LinearMap.BilinForm.apply_eq_dotProduct_toMatrix_mulVec`. -/
BilinForm.apply_eq_dotProduct_toMatrix_mulVec : ∀ {R₁ : Type u_1} {M₁ : Type u_2} [inst : CommSemiring R₁] [inst_1 : AddCommMonoid M₁] [inst_2 : Module R₁ M₁]
  {n : Type u_5} [inst_3 : Fintype n] [inst_4 : DecidableEq n] (b : Module.Basis n R₁ M₁)
  (B : LinearMap.BilinForm R₁ M₁) (x y : M₁),
  (B x) y = ⇑(b.repr x) ⬝ᵥ ((LinearMap.BilinForm.toMatrix b) B).mulVec ⇑(b.repr y)
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2to1.TrCfg.mk : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} {q : Option Λ} {v : σ} {S : (k : K) → List (Γ k)}
  (L : Turing.ListBlank ((k : K) → Option (Γ k))),
  (∀ (k : K), Turing.ListBlank.map (Turing.proj k) L = Turing.ListBlank.mk (List.map some (S k)).reverse) →
    Turing.TM2to1.TrCfg { l := q, var := v, stk := S }
      { l := Option.map Turing.TM2to1.Λ'.normal q, var := v, Tape := Turing.Tape.mk' ∅ (Turing.TM2to1.addBottom L) }
-- Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
MvPolynomial.esymmAlgHom_fin_injective : ∀ (R : Type u_3) {n m : ℕ} [inst : CommRing R], n ≤ m → Function.Injective ⇑(MvPolynomial.esymmAlgHom (Fin m) R n)
-- Mathlib.Algebra.Group.Submonoid.Defs
AddSubmonoidClass.mk_nsmul : ∀ {M : Type u_5} [inst : AddMonoid M] {A : Type u_4} [inst_1 : SetLike A M] [inst_2 : AddSubmonoidClass A M] {S : A}
  (x : M) (hx : x ∈ S) (n : ℕ), n • ⟨x, hx⟩ = ⟨n • x, ⋯⟩
-- Mathlib.Data.Ordmap.Invariants
Ordnode.Sized.dual_iff : ∀ {α : Type u_1} {t : Ordnode α}, t.dual.Sized ↔ t.Sized
-- Mathlib.GroupTheory.Perm.Cycle.Type
Equiv.Perm.isCycle_of_prime_order'' : ∀ {α : Type u_1} [inst : Fintype α] {σ : Equiv.Perm α},
  Nat.Prime (Fintype.card α) → orderOf σ = Fintype.card α → σ.IsCycle
-- Mathlib.Combinatorics.SetFamily.KruskalKatona
/-- The main Kruskal-Katona helper: use induction with our measure to keep compressing until
we can't any more, which gives a set family which is fully compressed and has the nice properties we
want.  -/
_private.Mathlib.Combinatorics.SetFamily.KruskalKatona.0.Finset.UV.kruskal_katona_helper : ∀ {n r : ℕ} (𝒜 : Finset (Finset (Fin n))),
  Set.Sized r ↑𝒜 →
    ∃ ℬ,
      ℬ.shadow.card ≤ 𝒜.shadow.card ∧
        𝒜.card = ℬ.card ∧
          Set.Sized r ↑ℬ ∧ ∀ (U V : Finset (Fin n)), Finset.UV.UsefulCompression✝ U V → UV.IsCompressed U V ℬ
-- Mathlib.GroupTheory.MonoidLocalization.Basic
AddSubmonoid.LocalizationMap.mk'_self : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N]
  (f : S.LocalizationMap N) (x : M) (H : x ∈ S), f.mk' x ⟨x, H⟩ = 0
-- Std.Data.HashMap.Lemmas
Std.HashMap.getElem?_filterMap : ∀ {α : Type u} {β : Type v} {γ : Type w} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {f : α → β → Option γ} {k : α},
  (Std.HashMap.filterMap f m)[k]? = m[k]?.pbind fun x_2 h' => f (m.getKey k ⋯) x_2
-- Mathlib.Order.Filter.Bases.Basic
Filter.hasBasis_self : ∀ {α : Type u_1} {l : Filter α} {P : Set α → Prop}, l.HasBasis (fun s => s ∈ l ∧ P s) id ↔ ∀ t ∈ l, ∃ r ∈ l, P r ∧ r ⊆ t
-- Lean.Elab.InfoTree.Main
Lean.Elab.CustomInfo.format : Lean.Elab.CustomInfo → Std.Format
-- Mathlib.Topology.MetricSpace.ProperSpace
/-- In a proper pseudometric space, any sphere is a `CompactSpace` when considered as a subtype.  -/
Metric.sphere.compactSpace : ∀ {α : Type u_3} [inst : PseudoMetricSpace α] [ProperSpace α] (x : α) (r : ℝ), CompactSpace ↑(Metric.sphere x r)
-- Mathlib.Data.Set.Lattice
Set.iUnion_union : ∀ {β : Type u_2} {ι : Sort u_5} [Nonempty ι] (s : Set β) (t : ι → Set β), (⋃ i, t i) ∪ s = ⋃ i, t i ∪ s
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.addZ_smul : ∀ {R : Type r} [inst : CommRing R] (P Q : Fin 3 → R) (u v : R),
  WeierstrassCurve.Jacobian.addZ (u • P) (v • Q) = (u * v) ^ 2 * WeierstrassCurve.Jacobian.addZ P Q
-- Mathlib.Topology.Bases
TopologicalSpace.instSeparableSpaceQuot : ∀ {α : Type u} [t : TopologicalSpace α] [TopologicalSpace.SeparableSpace α] {r : α → α → Prop},
  TopologicalSpace.SeparableSpace (Quot r)
-- Std.Data.Iterators.Lemmas.Producers.Monadic.Empty
Std.IterM.toListRev_empty : ∀ {m : Type u_1 → Type u_2} {β : Type u_1} [inst : Monad m] [LawfulMonad m], (Std.IterM.empty m β).toListRev = pure []
-- Init.Data.Array.OfFn
Array.ofFnM_pure : ∀ {m : Type u_1 → Type u_2} {α : Type u_1} [inst : Monad m] [LawfulMonad m] {n : ℕ} {f : Fin n → α},
  (Array.ofFnM fun i => pure (f i)) = pure (Array.ofFn f)
-- Mathlib.Algebra.Category.Semigrp.Basic
/-- Typecheck an `AddHom` as a morphism in `AddMagmaCat`.  -/
AddMagmaCat.ofHom : {X Y : Type u} → [inst : Add X] → [inst_1 : Add Y] → (X →ₙ+ Y) → (AddMagmaCat.of X ⟶ AddMagmaCat.of Y)
-- Mathlib.Topology.Algebra.Monoid
ContinuousAdd.induced : ∀ {α : Type u_6} {β : Type u_7} {F : Type u_8} [inst : FunLike F α β] [inst_1 : Add α] [inst_2 : Add β]
  [AddHomClass F α β] [tβ : TopologicalSpace β] [ContinuousAdd β] (f : F), ContinuousAdd α
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- Naturality of the `prodComparison` morphism in a natural transformation.  -/
CategoryTheory.Limits.prodComparison_natural_of_natTrans_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{w, u₂} D]
  {F : CategoryTheory.Functor C D} {A B : C} [inst_2 : CategoryTheory.Limits.HasBinaryProduct A B]
  [inst_3 : CategoryTheory.Limits.HasBinaryProduct (F.obj A) (F.obj B)] {H : CategoryTheory.Functor C D}
  [inst_4 : CategoryTheory.Limits.HasBinaryProduct (H.obj A) (H.obj B)] (α : F ⟶ H) {Z : D} (h : H.obj A ⨯ H.obj B ⟶ Z),
  CategoryTheory.CategoryStruct.comp (α.app (A ⨯ B))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prodComparison H A B) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prodComparison F A B)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map (α.app A) (α.app B)) h)
-- Mathlib.RingTheory.MvPowerSeries.Substitution
MvPowerSeries.subst_eq_eval₂ : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommRing R] {τ : Type u_4} {S : Type u_5} [inst_1 : CommRing S]
  [inst_2 : Algebra R S] [inst_3 : UniformSpace R] [DiscreteUniformity R] [inst_5 : UniformSpace S]
  [DiscreteUniformity S], MvPowerSeries.subst = MvPowerSeries.eval₂ (algebraMap R (MvPowerSeries τ S))
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.EMatchTheoremKind.default.inj : ∀ {gen gen_1 : Bool},
  Lean.Meta.Grind.EMatchTheoremKind.default gen = Lean.Meta.Grind.EMatchTheoremKind.default gen_1 → gen = gen_1
-- Init.SizeOf
PProd.mk.sizeOf_spec : ∀ {α : Sort u} {β : Sort v} [inst : SizeOf α] [inst_1 : SizeOf β] (fst : α) (snd : β),
  sizeOf ⟨fst, snd⟩ = 1 + sizeOf fst + sizeOf snd