mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.CharP.Lemmas
add_pow_expChar : ∀ {R : Type u_1} [inst : CommSemiring R] (x y : R) (p : ℕ) [hR : ExpChar R p], (x + y) ^ p = x ^ p + y ^ p
-- Mathlib.RingTheory.Spectrum.Prime.FreeLocus
Module.rankAtStalk_eq_finrank_tensorProduct : ∀ {R : Type uR} {M : Type uM} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (p : PrimeSpectrum R),
  Module.rankAtStalk M p =
    Module.finrank (Localization.AtPrime p.asIdeal) (TensorProduct R (Localization.AtPrime p.asIdeal) M)
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.AbsolutelyContinuous.sub : ∀ {α : Type u_1} {m : MeasurableSpace α} {N : Type u_5} [inst : AddCommMonoid N] [inst_1 : TopologicalSpace N]
  {M : Type u_6} [inst_2 : AddCommGroup M] [inst_3 : TopologicalSpace M] [inst_4 : IsTopologicalAddGroup M]
  {v₁ v₂ : MeasureTheory.VectorMeasure α M} {w : MeasureTheory.VectorMeasure α N},
  v₁.AbsolutelyContinuous w → v₂.AbsolutelyContinuous w → (v₁ - v₂).AbsolutelyContinuous w
-- Mathlib.Dynamics.PeriodicPts.Defs
_private.Mathlib.Dynamics.PeriodicPts.Defs.0.Function.minimalPeriod_iterate_eq_div_gcd_aux : ∀ {α : Type u_1} {f : α → α} {x : α} {n : ℕ},
  0 < (Function.minimalPeriod f x).gcd n →
    Function.minimalPeriod f^[n] x = Function.minimalPeriod f x / (Function.minimalPeriod f x).gcd n
-- Std.Data.DHashMap.Basic
Std.DHashMap.mk.injEq : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (inner : Std.DHashMap.Raw α β) (wf : inner.WF)
  (inner_1 : Std.DHashMap.Raw α β) (wf_1 : inner_1.WF),
  ({ inner := inner, wf := wf } = { inner := inner_1, wf := wf_1 }) = (inner = inner_1)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SemanticTokenModifier.abstract : Lean.Lsp.SemanticTokenModifier
-- Mathlib.Order.BooleanAlgebra.Basic
top_sdiff : ∀ {α : Type u} {x : α} [inst : BooleanAlgebra α], ⊤ \ x = xᶜ
-- Mathlib.Algebra.Module.Hom
AddMonoid.End.instDistribSMul : {M : Type u_3} → {A : Type u_4} → [inst : AddCommMonoid A] → [DistribSMul M A] → DistribSMul M (AddMonoid.End A)
-- Mathlib.Data.Finset.Lattice.Basic
Finset.union_union_union_comm : ∀ {α : Type u_1} [inst : DecidableEq α] (s t u v : Finset α), s ∪ t ∪ (u ∪ v) = s ∪ u ∪ (t ∪ v)
-- Mathlib.RingTheory.AdicCompletion.Completeness
AdicCompletion.ofPowSMul_val_apply : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {a b c : ℕ} (h : c = b + a) {x : AdicCompletion I ↥(I ^ a • ⊤)},
  ↑((AdicCompletion.ofPowSMul I M a) x) c = (Submodule.powSMulQuotInclusion I M h ⊤) (↑x b)
-- Init.Meta.Defs
Lean.Syntax.isToken : String → Lean.Syntax → Bool
-- Lean.Elab.DocString
/-- Retrieves the next positional argument from the arguments to a documentation extension. Throws
an error if no positional arguments remain.
 -/
Lean.Doc.getPositional : {α : Type} → [Lean.Doc.FromDocArg α] → Lean.Name → StateT (Array (Lean.TSyntax `doc_arg)) Lean.Doc.DocM α
-- Mathlib.Algebra.Algebra.Unitization
/-- The canonical inclusion `R → Unitization R A`.  -/
Unitization.inl : {R : Type u_1} → {A : Type u_2} → [Zero A] → R → Unitization R A
-- Lean.Meta.Injective
_private.Lean.Meta.Injective.0.Lean.Meta.solveEqOfCtorEq : Lean.Name → Lean.MVarId → Lean.FVarId → Lean.MetaM Unit
-- Mathlib.Geometry.Manifold.Notation
Manifold.Elab.FindModelResult.mk.injEq : ∀ (model : Lean.Expr) (normedSpaceInfo? : Option Manifold.Elab.NormedSpaceInfo) (model_1 : Lean.Expr)
  (normedSpaceInfo?_1 : Option Manifold.Elab.NormedSpaceInfo),
  ({ model := model, normedSpaceInfo? := normedSpaceInfo? } =
      { model := model_1, normedSpaceInfo? := normedSpaceInfo?_1 }) =
    (model = model_1 ∧ normedSpaceInfo? = normedSpaceInfo?_1)
-- Mathlib.Order.Filter.AtTopBot.Prod
Filter.Tendsto.prod_atTop : ∀ {α : Type u_3} {γ : Type u_5} [inst : Preorder α] [inst_1 : Preorder γ] {f g : α → γ},
  Filter.Tendsto f Filter.atTop Filter.atTop →
    Filter.Tendsto g Filter.atTop Filter.atTop → Filter.Tendsto (Prod.map f g) Filter.atTop Filter.atTop
-- Mathlib.Algebra.Group.Defs
npowBinRec.go_spec : ∀ {M : Type u_2} [inst : Semigroup M] [inst_1 : One M] (k : ℕ) (m n : M),
  npowBinRec.go (k + 1) m n = m * npowRec' (k + 1) n
-- Lean.Data.Options
Lean.Options.instBEq : BEq Lean.Options
-- Mathlib.MeasureTheory.Measure.AEMeasurable
aemeasurable_id'' : ∀ {α : Type u_2} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) {m : MeasurableSpace α},
  m ≤ m0 → AEMeasurable id μ
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
CategoryTheory.Limits.ι_colimitOfIsReflexivePairIsoCoequalizer_hom_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A B : C} {f g : A ⟶ B}
  [inst_1 : CategoryTheory.IsReflexivePair f g] [h : CategoryTheory.Limits.HasCoequalizer f g] {Z : C}
  (h_1 : CategoryTheory.Limits.coequalizer f g ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.colimit.ι (CategoryTheory.Limits.ofIsReflexivePair f g)
        CategoryTheory.Limits.WalkingReflexivePair.zero)
      (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.colimitOfIsReflexivePairIsoCoequalizer.hom h_1) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coequalizer.π f g) h_1
-- Mathlib.CategoryTheory.Sites.Over
CategoryTheory.Over.mapCongr.congr_simp : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X Y : T} (f g : X ⟶ Y) (h : f = g),
  CategoryTheory.Over.mapCongr f g h = CategoryTheory.Over.mapCongr f g h
-- Lean.DocString.Types
/-- The math content is set apart from the text flow, with more space.  -/
Lean.Doc.MathMode.display : Lean.Doc.MathMode
-- Mathlib.LinearAlgebra.FreeModule.Int
Int.addSubgroup_index_ne_zero_iff : ∀ {ι : Type u_1} [Finite ι] {H : AddSubgroup (ι → ℤ)}, H.index ≠ 0 ↔ Nonempty (↥H ≃+ (ι → ℤ))
-- Mathlib.Topology.UniformSpace.LocallyUniformConvergence
TendstoUniformlyOn.tendstoLocallyUniformlyOn : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : TopologicalSpace α] [inst_1 : UniformSpace β] {F : ι → α → β}
  {f : α → β} {s : Set α} {p : Filter ι}, TendstoUniformlyOn F f p s → TendstoLocallyUniformlyOn F f p s
-- Lean.Server.References
_private.Lean.Server.References.0.Lean.Server.combineIdents.useConstRepresentatives : Std.HashMap Lean.Lsp.RefIdent Lean.Lsp.RefIdent → Std.HashMap Lean.Lsp.RefIdent Lean.Lsp.RefIdent
-- Init.Data.List.Basic
/-- Returns the last element in the list, or `fallback` if the list is empty.

Alternatives include `List.getLast?`, which returns an `Option`, and `List.getLast!`, which panics
on empty lists.

Examples:
 * `["circle", "rectangle"].getLastD "oval" = "rectangle"`
 * `["circle"].getLastD "oval" = "circle"`
 * `([] : List String).getLastD "oval" = "oval"`
 -/
List.getLastD : {α : Type u} → List α → α → α
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.coeff_map : ∀ {R : Type u} {S₁ : Type v} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁] (f : R →+* S₁)
  (p : MvPolynomial σ R) (m : σ →₀ ℕ), MvPolynomial.coeff m ((MvPolynomial.map f) p) = f (MvPolynomial.coeff m p)
-- Mathlib.Probability.Martingale.BorelCantelli
/-- Auxiliary definition required to prove Lévy's generalization of the Borel-Cantelli lemmas for
which we will take the martingale part.  -/
MeasureTheory.BorelCantelli.process : {Ω : Type u_2} → (ℕ → Set Ω) → ℕ → Ω → ℝ
-- Mathlib.Combinatorics.Graph.Subgraph
Graph.IsClosedSubgraph.isInducedSubgraph : ∀ {α : Type u_1} {β : Type u_2} {H G : Graph α β}, H.IsClosedSubgraph G → H.IsInducedSubgraph G
-- Mathlib.Analysis.Calculus.ContDiff.Basic
/-- The Cartesian product of `C^n` functions at a point is `C^n`.  -/
ContDiffAt.prodMk : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {x : E} {n : WithTop ℕ∞} {f : E → F} {g : E → G},
  ContDiffAt 𝕜 n f x → ContDiffAt 𝕜 n g x → ContDiffAt 𝕜 n (fun x => (f x, g x)) x
-- Mathlib.GroupTheory.Perm.Cycle.Basic
Equiv.Perm.IsCycleOn.range_pow : ∀ {α : Type u_2} {f : Equiv.Perm α} {s : Set α} {a : α},
  s.Finite → f.IsCycleOn s → a ∈ s → (Set.range fun n => (f ^ n) a) = s
-- Mathlib.Data.PFun
PFun.coe_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (g : β → γ) (f : α → β), ↑(g ∘ f) = (↑g).comp ↑f
-- Lean.Parser.Extension
Lean.Parser.ParserExtension.Entry.kind.sizeOf_spec : ∀ (val : Lean.SyntaxNodeKind), sizeOf (Lean.Parser.ParserExtension.Entry.kind val) = 1 + sizeOf val
-- Mathlib.Algebra.Group.Defs
/-- Multiplication by `(0 : ℕ)` gives `0`.  -/
AddMonoid.nsmul_zero : ∀ {M : Type u} [self : AddMonoid M] (x : M), 0 • x = 0
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
CategoryTheory.Limits.ChosenPullback₃.p₂₃_p₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X₁ X₂ X₃ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S} {f₃ : X₃ ⟶ S}
  {h₁₂ : CategoryTheory.Limits.ChosenPullback f₁ f₂} {h₂₃ : CategoryTheory.Limits.ChosenPullback f₂ f₃}
  {h₁₃ : CategoryTheory.Limits.ChosenPullback f₁ f₃} (h : CategoryTheory.Limits.ChosenPullback₃ h₁₂ h₂₃ h₁₃),
  CategoryTheory.CategoryStruct.comp h.p₂₃ h₂₃.p₂ = h.p₃
-- Batteries.Data.List.Basic
List.foldrIdx.eq_2 : ∀ {α : Type u} {β : Type v} (f : ℕ → α → β → β) (init : β) (x : ℕ) (b : α) (l : List α),
  List.foldrIdx f init (b :: l) x = f x b (List.foldrIdx f init l (x + 1))
-- Mathlib.LinearAlgebra.Basis.VectorSpace
/-- If `s` is a linear independent set of vectors, we can extend it to a basis.  -/
Module.Basis.extend : {K : Type u_3} →
  {V : Type u_4} →
    [inst : DivisionRing K] →
      [inst_1 : AddCommGroup V] →
        [inst_2 : Module K V] → {s : Set V} → (hs : LinearIndepOn K id s) → Module.Basis (↑(hs.extend ⋯)) K V
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
groupCohomology.mapShortComplexH1_comp : ∀ {k : Type u} [inst : CommRing k] {G H K : Type u} [inst_1 : Group G] [inst_2 : Group H] [inst_3 : Group K]
  {A : Rep.{max u u_1, u, u} k K} {B : Rep.{max u u_1, u, u} k H} {C : Rep.{max u u_1, u, u} k G} (f : H →* K)
  (g : G →* H) (φ : Rep.res f A ⟶ B) (ψ : Rep.res g B ⟶ C),
  groupCohomology.mapShortComplexH1 (f.comp g) (CategoryTheory.CategoryStruct.comp ((Rep.resFunctor g).map φ) ψ) =
    CategoryTheory.CategoryStruct.comp (groupCohomology.mapShortComplexH1 f φ) (groupCohomology.mapShortComplexH1 g ψ)
-- Std.Time.Time.Unit.Minute
/-- Creates an `Offset` from a natural number.
 -/
Std.Time.Minute.Offset.ofNat : ℕ → Std.Time.Minute.Offset
-- Mathlib.Order.Interval.Set.Image
directedOn_ge_Ici : ∀ {α : Type u_1} [inst : Preorder α] (a : α), DirectedOn (fun x1 x2 => x1 ≥ x2) (Set.Ici a)
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Functor.Full.mapAddGrp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  {F : CategoryTheory.Functor C D} [inst_4 : F.Monoidal] [F.Full] [F.Faithful], F.mapAddGrp.Full
-- Mathlib.Tactic.CategoryTheory.Bicategory.Datatypes
Mathlib.Tactic.Bicategory.Context.mk.injEq : ∀ (level₂ level₁ level₀ : Lean.Level) (B : Q(Type level₀)) (instBicategory : Q(CategoryTheory.Bicategory «$B»))
  (level₂_1 level₁_1 level₀_1 : Lean.Level) (B_1 : Q(Type level₀_1))
  (instBicategory_1 : Q(CategoryTheory.Bicategory «$B_1»)),
  ({ level₂ := level₂, level₁ := level₁, level₀ := level₀, B := B, instBicategory := instBicategory } =
      { level₂ := level₂_1, level₁ := level₁_1, level₀ := level₀_1, B := B_1, instBicategory := instBicategory_1 }) =
    (level₂ = level₂_1 ∧ level₁ = level₁_1 ∧ level₀ = level₀_1 ∧ B = B_1 ∧ instBicategory = instBicategory_1)
-- Lean.Parser.Attr
Lean.Parser.Attr.macro.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Order.Partition.Basic
/-- Any element of a part is related to the representative of that part.  -/
Partition.rep_rel : ∀ {α : Type u_1} {x : α} {u t : Set α} {P : Partition u} (ht : t ∈ P), x ∈ t → P.Rel x (P.rep ht)
-- Mathlib.Order.Cover
CovBy.Ico_eq : ∀ {α : Type u_1} [inst : PartialOrder α] {a b : α}, a ⋖ b → Set.Ico a b = {a}
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.arrowCongr_refl : ∀ {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Semiring A₂]
  [inst_3 : Algebra R A₁] [inst_4 : Algebra R A₂], AlgEquiv.refl.arrowCongr AlgEquiv.refl = Equiv.refl (A₁ →ₐ[R] A₂)
-- Mathlib.Data.Multiset.MapFold
/-- `foldr f H b s` is the lift of the list operation `foldr f b l`,
which folds `f` over the multiset. It is well defined when `f` is left-commutative,
that is, `f a₁ (f a₂ b) = f a₂ (f a₁ b)`.  -/
Multiset.foldr : {α : Type u_1} → {β : Type v} → (f : α → β → β) → [LeftCommutative f] → β → Multiset α → β
-- Mathlib.Data.Finite.Defs
Finite.intro : ∀ {α : Sort u_3} {n : ℕ} (a : α ≃ Fin n), Finite α
-- Mathlib.Algebra.Group.Defs
DivisionMonoid.inv_inv : ∀ {G : Type u} [self : DivisionMonoid G] (x : G), x⁻¹⁻¹ = x
-- Mathlib.Logic.Embedding.Basic
/-- Surjective embeddings are equivalent to equivalences.  -/
Equiv.embeddingSurjectiveEquiv : {α : Sort u_1} → {β : Type u_2} → { f // Function.Surjective ⇑f } ≃ (α ≃ β)
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.interFst_toHom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreOneHypercover S)
  (F : CategoryTheory.PreOneHypercover S)
  [inst_1 : ∀ (i : E.I₀) (j : F.I₀), CategoryTheory.Limits.HasPullback (E.f i) (F.f j)]
  [inst_2 :
    ∀ (i j : E.I₀) (k : E.I₁ i j) (a b : F.I₀) (l : F.I₁ a b),
      CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (E.p₁ k) (E.f i))
        (CategoryTheory.CategoryStruct.comp (F.p₁ l) (F.f a))],
  (E.interFst F).toHom = E.interFst F.toPreZeroHypercover
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.getKeyD_insertManyIfNewUnit_list_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α fun x => Unit} [EquivBEq α] [LawfulHashable α]
  {l : List α} {k fallback : α},
  k ∈ m → (Std.DHashMap.Const.insertManyIfNewUnit m l).getKeyD k fallback = m.getKeyD k fallback
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.all_eq_not_any_not : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α]
  {p : (a : α) → β a → Bool}, m.WF → m.all p = !m.any fun a b => !p a b
-- Init.Data.BitVec.Lemmas
/-- Accessing bits in `x.rotateLeft r` the range `[r, w)` is equal to
accessing bits `x` in the range `[0, w - r)`.

Proof by example:
Let x := <6 5 4 3 2 1 0> : BitVec 7.
x.rotateLeft 2 = (<6 5 | 4 3 2 1 0>).rotateLeft 2 = <3 2 1 0 | 6 5>

(x.rotateLeft 2).getLsbD ⟨i, i ≥ 2⟩
= <3 2 1 0 | 6 5>.getLsbD ⟨i, i ≥ 2⟩
= <3 2 1 0>[i - 2]
= <6 5 | 3 2 1 0>[i - 2]

Intuitively, grab the full width (7), then move the marker `|` by `r` to the right `(-2)`
Then, access the bit at `i` from the right `(+i)`.
  -/
BitVec.getLsbD_rotateLeftAux_of_ge : ∀ {w : ℕ} {x : BitVec w} {r i : ℕ}, i ≥ r → (x.rotateLeftAux r).getLsbD i = (decide (i < w) && x.getLsbD (i - r))
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.isEmpty_modify : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α],
  t.WF → ∀ {k : α} {f : β k → β k}, (Std.DTreeMap.Internal.Impl.modify k f t).isEmpty = t.isEmpty
-- Init.Data.String.Lemmas.Splits
String.Slice.Pos.Splits.copy_sliceFrom_eq : ∀ {t₁ t₂ : String} {s : String.Slice} {p : s.Pos}, p.Splits t₁ t₂ → (s.sliceFrom p).copy = t₂
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.pullback₁_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S T : C} (f : S ⟶ T) (E : CategoryTheory.PreZeroHypercover T)
  [inst_1 : ∀ (i : E.I₀), CategoryTheory.Limits.HasPullback f (E.f i)] (x : E.I₀),
  (CategoryTheory.PreZeroHypercover.pullback₁ f E).f x = CategoryTheory.Limits.pullback.fst f (E.f x)
-- Mathlib.Data.Quot
Quotient.liftOn_mk : ∀ {α : Sort u_1} {β : Sort u_2} {s : Setoid α} (f : α → β) (h : ∀ (a b : α), a ≈ b → f a = f b) (x : α),
  ⟦x⟧.liftOn f h = f x
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.mem_insert_self : ∀ {α : Type u_1} {c : RBTree.RBColor} {n : ℕ} {cmp : α → α → Ordering} {v : α} {t : RBTree.RBNode α},
  t.Balanced c n → v ∈ RBTree.RBNode.insert cmp t v
-- Mathlib.MeasureTheory.Group.FoelnerFilter
/-- Consider a group `G` acting on a measure space `X`.
A sequence of sets `F : ι → Set X` is **Følner** with respect to the `G`-action,
the measure `μ`, and a filter `l` on the indexing type `ι`, if:
1. Each `s` in `l` is eventually measurable with finite non-zero measure,
2. For all `g : G`, `μ ((g • F i) ∆ F i) / μ (F i)` tends to `0`.  -/
IsFoelner : (G : Type u_1) →
  {X : Type u_2} →
    [inst : MeasurableSpace X] →
      MeasureTheory.Measure X → [inst : Group G] → [MulAction G X] → {ι : Type u_3} → Filter ι → (ι → Set X) → Prop
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.instInv : {α : Type u_1} →
  {γ : Type u_3} →
    [inst : MeasurableSpace α] →
      {μ : MeasureTheory.Measure α} →
        [inst_1 : TopologicalSpace γ] → [inst_2 : Group γ] → [IsTopologicalGroup γ] → Inv (α →ₘ[μ] γ)
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.IsModHom.smul_hom_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.MonoidalLeftAction C D}
  {A : C} {inst_4 : CategoryTheory.MonObj A} {M N : D} {inst_5 : CategoryTheory.ModObj A M}
  {inst_6 : CategoryTheory.ModObj A N} {f : M ⟶ N} [self : CategoryTheory.IsModHom A f] {Z : D} (h : N ⟶ Z),
  CategoryTheory.CategoryStruct.comp CategoryTheory.ModObj.smul (CategoryTheory.CategoryStruct.comp f h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight A f)
      (CategoryTheory.CategoryStruct.comp CategoryTheory.ModObj.smul h)
-- Lean.Meta.Match.MatchEqsExt
Lean.Meta.Match.MatchEqns.mk.injEq : ∀ (eqnNames : Array Lean.Name) (splitterName : Lean.Name) (splitterMatchInfo : Lean.Meta.MatcherInfo)
  (eqnNames_1 : Array Lean.Name) (splitterName_1 : Lean.Name) (splitterMatchInfo_1 : Lean.Meta.MatcherInfo),
  ({ eqnNames := eqnNames, splitterName := splitterName, splitterMatchInfo := splitterMatchInfo } =
      { eqnNames := eqnNames_1, splitterName := splitterName_1, splitterMatchInfo := splitterMatchInfo_1 }) =
    (eqnNames = eqnNames_1 ∧ splitterName = splitterName_1 ∧ splitterMatchInfo = splitterMatchInfo_1)
-- Mathlib.Analysis.InnerProductSpace.Defs
/-- Define `InnerProductSpace.Core` from `InnerProductSpace`. Defined to reuse lemmas about
`InnerProductSpace.Core` for `InnerProductSpace`s. Note that the `Norm` instance provided by
`InnerProductSpace.Core.norm` is propositionally but not definitionally equal to the original
norm.  -/
InnerProductSpace.toCore : {𝕜 : Type u_1} →
  {E : Type u_2} →
    [inst : RCLike 𝕜] → [inst_1 : NormedAddCommGroup E] → [c : InnerProductSpace 𝕜 E] → InnerProductSpace.Core 𝕜 E
-- Lean.Meta.Injective
_private.Lean.Meta.Injective.0.Lean.Meta.MkHInjTypeResult.mk.sizeOf_spec : ∀ (thmType : Lean.Expr) (us : List Lean.Level) (numIndices : ℕ),
  sizeOf { thmType := thmType, us := us, numIndices := numIndices } = 1 + sizeOf thmType + sizeOf us + sizeOf numIndices
-- Mathlib.CategoryTheory.Monoidal.Transport
CategoryTheory.Monoidal.InducingFunctorData.associator_eq : ∀ {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.MonoidalCategoryStruct D]
  {F : CategoryTheory.Functor D C} (self : CategoryTheory.Monoidal.InducingFunctorData F) (X Y Z : D),
  F.map (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom =
    (((self.μIso (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z).symm ≪≫
          CategoryTheory.MonoidalCategory.tensorIso (self.μIso X Y).symm (CategoryTheory.Iso.refl (F.obj Z))) ≪≫
        CategoryTheory.MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z) ≪≫
          CategoryTheory.MonoidalCategory.tensorIso (CategoryTheory.Iso.refl (F.obj X)) (self.μIso Y Z) ≪≫
            self.μIso X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)).hom
-- Mathlib.Data.String.Basic
String.ofList_eq : ∀ {l : List Char} {s : String}, String.ofList l = s ↔ l = s.toList
-- Aesop.Tree.TreeM
Aesop.incrementNumGoals : optParam ℕ 1 → Aesop.TreeM Unit
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.EMatchDiagInfo.mk.sizeOf_spec : ∀ (lctx : Lean.LocalContext) (sources : List Lean.Meta.Grind.EMatchDiagNode) (target : Lean.Meta.Grind.EMatchDiagNode),
  sizeOf { lctx := lctx, sources := sources, target := target } = 1 + sizeOf lctx + sizeOf sources + sizeOf target
-- Init.Data.List.Sort.Lemmas
_private.Init.Data.List.Sort.Lemmas.0.List.merge.eq_2 : ∀ {α : Type u_1} (xs : List α) (le : α → α → Bool), (xs = [] → False) → xs.merge [] le = xs
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
/-- `Prod.map` of two continuous linear maps.  -/
ContinuousLinearMap.prodMap : {R : Type u_1} →
  [inst : Semiring R] →
    {M₁ : Type u_2} →
      [inst_1 : TopologicalSpace M₁] →
        [inst_2 : AddCommMonoid M₁] →
          [inst_3 : Module R M₁] →
            {M₂ : Type u_3} →
              [inst_4 : TopologicalSpace M₂] →
                [inst_5 : AddCommMonoid M₂] →
                  [inst_6 : Module R M₂] →
                    {M₃ : Type u_4} →
                      [inst_7 : TopologicalSpace M₃] →
                        [inst_8 : AddCommMonoid M₃] →
                          [inst_9 : Module R M₃] →
                            {M₄ : Type u_5} →
                              [inst_10 : TopologicalSpace M₄] →
                                [inst_11 : AddCommMonoid M₄] →
                                  [inst_12 : Module R M₄] → (M₁ →L[R] M₂) → (M₃ →L[R] M₄) → M₁ × M₃ →L[R] M₂ × M₄
-- Mathlib.Order.CompleteLattice.Lemmas
ULift.infSet.eq_1 : ∀ {α : Type u_1} [inst : InfSet α], ULift.infSet = { sInf := fun s => { down := sInf (ULift.up ⁻¹' s) } }
-- Mathlib.LinearAlgebra.Finsupp.Defs
/-- **Alias** of `Finsupp.curryLinearEquiv`.

---

The linear equivalence between `α × β →₀ M` and `α →₀ β →₀ M`.

This is the `LinearEquiv` version of `Finsupp.curryEquiv`.  -/
Finsupp.finsuppProdLEquiv : {α : Type u_9} →
  {β : Type u_10} →
    (R : Type u_11) →
      {M : Type u_12} →
        [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → (α × β →₀ M) ≃ₗ[R] α →₀ β →₀ M
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
/-- The cokernel built from `cokernel.π f` is colimiting.  -/
CategoryTheory.Limits.cokernelIsCokernel : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y : C} →
        (f : X ⟶ Y) →
          [inst_2 : CategoryTheory.Limits.HasCokernel f] →
            CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofork.ofπ (CategoryTheory.Limits.cokernel.π f) ⋯)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.constGetEntryLED_eq : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t₁ t₂ : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  t₁.WF →
    t₂.WF →
      t₁.Equiv t₂ →
        ∀ {k : α} {fallback : α × β},
          Std.DTreeMap.Internal.Impl.Const.getEntryLED k t₁ fallback =
            Std.DTreeMap.Internal.Impl.Const.getEntryLED k t₂ fallback
-- Init.Data.Array.Range
Array.zipIdx_eq_append_iff : ∀ {α : Type u_1} {ys zs : Array (α × ℕ)} {xs : Array α} {k : ℕ},
  xs.zipIdx k = ys ++ zs ↔ ∃ ys' zs', xs = ys' ++ zs' ∧ ys = ys'.zipIdx k ∧ zs = zs'.zipIdx (k + ys'.size)
-- Aesop.Rule.Name
Aesop.RuleName.scope : Aesop.RuleName → Aesop.ScopeName
-- Mathlib.LinearAlgebra.Eigenspace.Basic
Module.End.eigenspace.eq_1 : ∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (f : Module.End R M)
  (μ : R), f.eigenspace μ = (f.genEigenspace μ) 1
-- Init.Internal.Order.Lemmas
Lean.Order.Array.monotone_modifyM : ∀ {m : Type u → Type v} [inst : Monad m] [inst_1 : (α : Type u) → Lean.Order.PartialOrder (m α)] [Lean.Order.MonoBind m]
  {α : Type u} {γ : Type w} [inst_3 : Lean.Order.PartialOrder γ] (a : Array α) (i : ℕ) (f : γ → α → m α),
  Lean.Order.monotone f → Lean.Order.monotone fun x => a.modifyM i (f x)