mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Combinatorics.SimpleGraph.Cayley
SimpleGraph.addCayley_union : ∀ {M : Type u_1} [inst : Add M] (s₁ s₂ : Set M),
  SimpleGraph.addCayley (s₁ ∪ s₂) = SimpleGraph.addCayley s₁ ⊔ SimpleGraph.addCayley s₂
-- Lean.Server.Requests
Lean.Server.RequestM.bindRequestTaskCostly : {α : Type u_1} →
  {β : Type} →
    Lean.Server.RequestTask α →
      (α → Lean.Server.RequestM (Lean.Server.RequestTask β)) → Lean.Server.RequestM (Lean.Server.RequestTask β)
-- Mathlib.NumberTheory.SelbergSieve
BoundingSieve.selbergTerms_isMultiplicative : ∀ {s : BoundingSieve}, BoundingSieve.selbergTerms.IsMultiplicative
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
Measurable.subtype_map : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α → β} {p : α → Prop}
  {q : β → Prop}, Measurable f → ∀ (hpq : ∀ (x : α), p x → q (f x)), Measurable (Subtype.map f hpq)
-- Mathlib.CategoryTheory.Pi.Monoidal
CategoryTheory.Pi.associator_inv_apply : ∀ {I : Type w₁} {C : I → Type u₁} [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)]
  [inst_1 : (i : I) → CategoryTheory.MonoidalCategory (C i)] {X Y Z : (i : I) → C i} {i : I},
  (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv i =
    (CategoryTheory.MonoidalCategoryStruct.associator (X i) (Y i) (Z i)).inv
-- Mathlib.Algebra.Lie.Extension
/-- `L` is a Lie algebra over `R`.  -/
LieAlgebra.Extension.instLieAlgebra : {R : Type u_1} →
  {N : Type u_2} →
    {M : Type u_4} →
      [inst : CommRing R] →
        [inst_1 : LieRing N] →
          [inst_2 : LieAlgebra R N] →
            [inst_3 : LieRing M] → [inst_4 : LieAlgebra R M] → (self : LieAlgebra.Extension R N M) → LieAlgebra R self.L
-- Mathlib.Algebra.Group.Hom.Defs
/-- Any type satisfying `AddMonoidHomClass` can be cast into `AddMonoidHom` via
`AddMonoidHomClass.toAddMonoidHom`.  -/
instCoeTCAddMonoidHomOfAddMonoidHomClass : {M : Type u_4} →
  {N : Type u_5} →
    {F : Type u_9} →
      [inst : AddZero M] →
        [inst_1 : AddZero N] → [inst_2 : FunLike F M N] → [AddMonoidHomClass F M N] → CoeTC F (M →+ N)
-- Mathlib.Analysis.Calculus.Deriv.Comp
HasFDerivAt.comp_hasDerivWithinAt : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {E : Type w} [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace 𝕜 E] {f : 𝕜 → F}
  {f' : F} (x : 𝕜) {s : Set 𝕜} {l : F → E} {l' : F →L[𝕜] E},
  HasFDerivAt l l' (f x) → HasDerivWithinAt f f' s x → HasDerivWithinAt (l ∘ f) (l' f') s x
-- Init.Data.Array.OfFn
List.toArray_ofFn : ∀ {n : ℕ} {α : Type u_1} {f : Fin n → α}, (List.ofFn f).toArray = Array.ofFn f
-- Init.Data.List.Basic
List.leftpadTR.eq_1 : ∀ {α : Type u} (n : ℕ) (a : α) (l : List α), List.leftpadTR n a l = List.replicateTR.loop a (n - l.length) l
-- Mathlib.CategoryTheory.Presentable.Directed
CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.DiagramWithUniqueTerminal.toDiagram : {J : Type w} →
  [inst : CategoryTheory.SmallCategory J] →
    {κ : Cardinal.{w}} →
      CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.DiagramWithUniqueTerminal J κ →
        CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram J κ
-- Mathlib.LinearAlgebra.TensorProduct.Defs
TensorProduct.tmul_single : ∀ {R : Type u_1} [inst : CommSemiring R] {N : Type u_8} [inst_1 : AddCommMonoid N] [inst_2 : Module R N] {ι : Type u_22}
  [inst_3 : DecidableEq ι] {M : ι → Type u_23} [inst_4 : (i : ι) → AddCommMonoid (M i)]
  [inst_5 : (i : ι) → Module R (M i)] (i : ι) (x : N) (m : M i) (j : ι),
  x ⊗ₜ[R] Pi.single i m j = Pi.single i (x ⊗ₜ[R] m) j
-- Init.Prelude
/-- Create array `#[a₁, a₂, a₃, a₄, a₅, a₆]`  -/
Array.mkArray6 : {α : Type u} → α → α → α → α → α → α → Array α
-- Mathlib.GroupTheory.MonoidLocalization.Basic
Submonoid.LocalizationMap.instCancelCommMonoidLocalization : {M : Type u_3} → [inst : CancelCommMonoid M] → (S : Submonoid M) → CancelCommMonoid (Localization S)
-- Mathlib.RingTheory.HahnSeries.HEval
PowerSeries.heval_apply : ∀ {Γ : Type u_1} {R : Type u_3} [inst : AddCommMonoid Γ] [inst_1 : LinearOrder Γ] [inst_2 : IsOrderedCancelAddMonoid Γ]
  [inst_3 : CommRing R] (x : HahnSeries Γ R) (f : PowerSeries R),
  (PowerSeries.heval x) f = (HahnSeries.SummableFamily.powerSeriesFamily x f).hsum
-- Init.Data.String.Lemmas.Splits
String.copy_sliceTo_eq_iff_splits : ∀ {s : String} {p : s.Pos} {t₁ : String}, (s.sliceTo p).copy = t₁ ↔ p.Splits t₁ (s.sliceFrom p).copy
-- Mathlib.Algebra.Category.Grp.Adjunctions
CommMonCat.val_inv_units_map_hom_apply : ∀ {X Y : CommMonCat} (f : X ⟶ Y) (u : (↑X)ˣ),
  ↑((CommGrpCat.Hom.hom (CommMonCat.units.map f)) u)⁻¹ = (CommMonCat.Hom.hom f) ↑u⁻¹
-- Mathlib.Algebra.Quandle
Rack.PreEnvelGroupRel'.congr_inv : {R : Type u} →
  [inst : Rack R] →
    {a a' : Rack.PreEnvelGroup R} → Rack.PreEnvelGroupRel' R a a' → Rack.PreEnvelGroupRel' R a.inv a'.inv
-- Init.Data.Int.Order
Int.sign_eq_one_iff_pos : ∀ {a : ℤ}, a.sign = 1 ↔ 0 < a
-- Lean.Data.Lsp.Extra
Lean.Lsp.instFromJsonLeanModuleHierarchyImportedByParams.fromJson : Lean.Json → Except String Lean.Lsp.LeanModuleHierarchyImportedByParams
-- Mathlib.Order.Filter.AtTopBot.Basic
/-- **Alias** of the forward direction of `Filter.eventually_atTop`. -/
Filter.Eventually.exists_forall_of_atTop : ∀ {α : Type u_3} [inst : Preorder α] [IsDirectedOrder α] {p : α → Prop} [Nonempty α],
  (∀ᶠ (x : α) in Filter.atTop, p x) → ∃ a, ∀ (b : α), a ≤ b → p b
-- Std.Internal.Do.Triple.SpecLemmas
/-- A termination measure for a `repeatM` loop.  -/
Std.Internal.Do.RepeatVariant : Type u → Type u
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.iSup_induction : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] {ι : Sort u_1} (N : ι → LieSubmodule R L M) {motive : M → Prop}
  {x : M},
  x ∈ ⨆ i, N i →
    (∀ (i : ι), ∀ y ∈ N i, motive y) → motive 0 → (∀ (y z : M), motive y → motive z → motive (y + z)) → motive x
-- Mathlib.Combinatorics.SimpleGraph.Finite
SimpleGraph.coe_neighborFinset : ∀ {V : Type u_1} (G : SimpleGraph V) (v : V) [inst : Fintype ↑(G.neighborSet v)],
  ↑(G.neighborFinset v) = G.neighborSet v
-- Mathlib.Order.Antisymmetrization
AntisymmRel.lt_congr_left : ∀ {α : Type u_1} {a b c : α} [inst : Preorder α], AntisymmRel (fun x1 x2 => x1 ≤ x2) a b → (a < c ↔ b < c)
-- Mathlib.CategoryTheory.Limits.ConeCategory
CategoryTheory.Limits.Cone.fromStructuredArrow_pt : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {D : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} D] (F : CategoryTheory.Functor C D) {X : D}
  (G : CategoryTheory.Functor J (CategoryTheory.StructuredArrow X F)),
  (CategoryTheory.Limits.Cone.fromStructuredArrow F G).pt = X
-- Mathlib.RingTheory.GradedAlgebra.RingHom
GradedRingHom.coe_one : ∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_6} [inst : Semiring A] [inst_1 : SetLike σ A] {𝒜 : ι → σ}, ⇑1 = id
-- Mathlib.Algebra.Group.Torsion
inv_ne_self : ∀ {G : Type u_2} [inst : Group G] [IsMulTorsionFree G] {a : G}, a⁻¹ ≠ a ↔ a ≠ 1
-- ProofWidgets.Component.HtmlDisplay
/-- Any term `t : α` with a `HtmlEval α` instance
can be evaluated in a `#html t` command.

This is analogous to how `Lean.MetaEval` supports `#eval`.  -/
ProofWidgets.HtmlEval : Type u → Type u
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
SimpleGraph.IsEdgeReachable.anti : ∀ {V : Type u_1} {G : SimpleGraph V} {k l : ℕ} {u v : V}, k ≤ l → G.IsEdgeReachable l u v → G.IsEdgeReachable k u v
-- Mathlib.Combinatorics.Additive.VerySmallDoubling
_private.Mathlib.Combinatorics.Additive.VerySmallDoubling.0.Finset.connectivity.congr_simp : ∀ {G : Type u_1} [inst : Group G] {inst_1 : DecidableEq G} [inst_2 : DecidableEq G] (K K_1 : ℝ),
  K = K_1 → ∀ (S S_1 : Finset G), S = S_1 → Finset.connectivity✝ K S = Finset.connectivity✝ K_1 S_1
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.self_le_max_insert : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [inst : Std.TransCmp cmp] {k : α},
  (cmp k ((t.insert k).max ⋯)).isLE = true
-- Aesop.Forward.PremiseIndex
Aesop.instLTPremiseIndex : LT Aesop.PremiseIndex
-- Mathlib.Topology.Sheaves.Presheaf
/-- The natural isomorphism between the pushforward of a presheaf along the identity continuous map
and the original presheaf.  -/
TopCat.Presheaf.Pushforward.id : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X : TopCat} →
      (ℱ : TopCat.Presheaf C X) → (TopCat.Presheaf.pushforward C (CategoryTheory.CategoryStruct.id X)).obj ℱ ≅ ℱ
-- Mathlib.Algebra.ContinuedFractions.Basic
/-- Returns the approximation of the fraction described by the given sequence up to a given position n.
For example, `convs'Aux [(1, 2), (3, 4), (5, 6)] 2 = 1 / (2 + 3 / 4)` and
`convs'Aux [(1, 2), (3, 4), (5, 6)] 0 = 0`.
 -/
GenContFract.convs'Aux : {K : Type u_2} → [DivisionRing K] → Stream'.Seq (GenContFract.Pair K) → ℕ → K
-- Mathlib.Topology.Order.OrderClosed
/-- The limit of a collection of functions that is frequently monotone on a set is monotone on
that set.  -/
monotoneOn_of_frequently_monotoneOn_of_tendsto : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : Preorder α] [t : OrderClosedTopology α] {ι : Type u_1}
  {l : Filter ι} [inst_2 : Preorder β] {F : ι → β → α} {f : β → α} {s : Set β},
  (∃ᶠ (i : ι) in l, MonotoneOn (F i) s) → (∀ x ∈ s, Filter.Tendsto (fun i => F i x) l (nhds (f x))) → MonotoneOn f s
-- Mathlib.Combinatorics.Digraph.Orientation
Digraph.toSimpleGraphStrict_top : ∀ {V : Type u_1}, ⊤.toSimpleGraphStrict = ⊤
-- Mathlib.MeasureTheory.Integral.Marginal
MeasureTheory.lmarginal_singleton : ∀ {δ : Type u_1} {X : δ → Type u_3} [inst : (i : δ) → MeasurableSpace (X i)] {μ : (i : δ) → MeasureTheory.Measure (X i)}
  [inst_1 : DecidableEq δ] (f : ((i : δ) → X i) → ENNReal) (i : δ),
  ∫⋯∫⁻_{i}, f ∂μ = fun x => ∫⁻ (xᵢ : X i), f (Function.update x i xᵢ) ∂μ i
-- Batteries.Data.String.Lemmas
_private.Batteries.Data.String.Lemmas.0.String.add_utf8Size_pos : ∀ {i : ℕ} {c : Char}, 0 < i + c.utf8Size
-- Mathlib.Topology.WithTopology
/-- If `X` is equipped with topology `t`, the map `X → WithTopology X t` is continuous.  -/
WithTopology.continuous_toTopology : ∀ {X : Type u_1} (t : TopologicalSpace X), Continuous (WithTopology.toTopology t)
-- Mathlib.Geometry.Manifold.VectorBundle.Hom
/-- Consider `C^n` maps `v : M → E₁` and `w : M → E₂` to vector bundles, over a base map
`b : M → B`, and bilinear maps `ψ m : E₁ (b m) → E₂ (b m) → E₃ (b m)` depending smoothly on `m`.
One can apply `ψ  m` to `v m` and `w m`, and the resulting map is `C^n`.  -/
ContMDiff.clm_bundle_apply₂ : ∀ {𝕜 : Type u_1} {B : Type u_2} {F₁ : Type u_3} {F₂ : Type u_4} {F₃ : Type u_5} {M : Type u_6}
  [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {E₁ : B → Type u_7} [inst_1 : (x : B) → AddCommGroup (E₁ x)]
  [inst_2 : (x : B) → Module 𝕜 (E₁ x)] [inst_3 : NormedAddCommGroup F₁] [inst_4 : NormedSpace 𝕜 F₁]
  [inst_5 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)] [inst_6 : (x : B) → TopologicalSpace (E₁ x)] {E₂ : B → Type u_8}
  [inst_7 : (x : B) → AddCommGroup (E₂ x)] [inst_8 : (x : B) → Module 𝕜 (E₂ x)] [inst_9 : NormedAddCommGroup F₂]
  [inst_10 : NormedSpace 𝕜 F₂] [inst_11 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)]
  [inst_12 : (x : B) → TopologicalSpace (E₂ x)] {E₃ : B → Type u_9} [inst_13 : (x : B) → AddCommGroup (E₃ x)]
  [inst_14 : (x : B) → Module 𝕜 (E₃ x)] [inst_15 : NormedAddCommGroup F₃] [inst_16 : NormedSpace 𝕜 F₃]
  [inst_17 : TopologicalSpace (Bundle.TotalSpace F₃ E₃)] [inst_18 : (x : B) → TopologicalSpace (E₃ x)] {EB : Type u_10}
  [inst_19 : NormedAddCommGroup EB] [inst_20 : NormedSpace 𝕜 EB] {HB : Type u_11} [inst_21 : TopologicalSpace HB]
  {IB : ModelWithCorners 𝕜 EB HB} [inst_22 : TopologicalSpace B] [inst_23 : ChartedSpace HB B] {EM : Type u_12}
  [inst_24 : NormedAddCommGroup EM] [inst_25 : NormedSpace 𝕜 EM] {HM : Type u_13} [inst_26 : TopologicalSpace HM]
  {IM : ModelWithCorners 𝕜 EM HM} [inst_27 : TopologicalSpace M] [inst_28 : ChartedSpace HM M]
  [inst_29 : FiberBundle F₁ E₁] [inst_30 : VectorBundle 𝕜 F₁ E₁] [inst_31 : FiberBundle F₂ E₂]
  [inst_32 : VectorBundle 𝕜 F₂ E₂] [inst_33 : FiberBundle F₃ E₃] [inst_34 : ⋯], ⋯
-- Std.Data.DHashMap.Internal.AssocList.Basic
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.AssocList.getEntry : {α : Type u} →
  {β : α → Type v} →
    [inst : BEq α] →
      (a : α) →
        (l : Std.DHashMap.Internal.AssocList α β) → Std.DHashMap.Internal.AssocList.contains a l = true → (a : α) × β a
-- Mathlib.Computability.AkraBazzi.SumTransform
AkraBazziRecurrence.eventually_r_le_b : ∀ {α : Type u_1} [inst : Fintype α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ} [inst_1 : Nonempty α]
  (R : AkraBazziRecurrence T g a b r), ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (i : α), ↑(r i n) ≤ b i * ↑n + ↑n / Real.log ↑n ^ 2
-- Std.Data.DHashMap.Basic
/-- Tries to retrieve the mapping for the given key, panicking if no such mapping is present.  -/
Std.DHashMap.Const.get! : {α : Type u} → {x : BEq α} → {x_1 : Hashable α} → {β : Type v} → [Inhabited β] → (Std.DHashMap α fun x => β) → α → β
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnSeries.leadingCoeff_mul_of_ne_zero : ∀ {Γ : Type u_1} {R : Type u_3} [inst : AddCommMonoid Γ] [inst_1 : LinearOrder Γ] [inst_2 : IsOrderedCancelAddMonoid Γ]
  [inst_3 : NonUnitalNonAssocSemiring R] {x y : HahnSeries Γ R},
  x.leadingCoeff * y.leadingCoeff ≠ 0 → (x * y).leadingCoeff = x.leadingCoeff * y.leadingCoeff
-- Mathlib.Data.Sum.Basic
Sum.update_inl_apply_inr : ∀ {α : Type u} {β : Type v} {γ : Type u_1} [inst : DecidableEq (α ⊕ β)] {f : α ⊕ β → γ} {i : α} {j : β} {x : γ},
  Function.update f (Sum.inl i) x (Sum.inr j) = f (Sum.inr j)
-- Mathlib.NumberTheory.ModularForms.SlashInvariantForms
/-- See note [custom simps projection].  -/
SlashInvariantForm.Simps.coe : (Γ : outParam (Subgroup (GL (Fin 2) ℝ))) → (k : outParam ℤ) → SlashInvariantForm Γ k → UpperHalfPlane → ℂ
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Pretrivialization.mk_proj_snd' : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  (e : Bundle.Pretrivialization F proj) {x : Z}, proj x ∈ e.baseSet → (proj x, (↑e x).2) = ↑e x
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.filter_equiv_self_iff : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α]
  {f : (a : α) → β a → Bool}, (Std.DHashMap.filter f m).Equiv m ↔ ∀ (k : α) (h : k ∈ m), f k (m.get k h) = true
-- Mathlib.Order.SymmDiff
bihimp_fst : ∀ {α : Type u_2} {β : Type u_3} [inst : GeneralizedHeytingAlgebra α] [inst_1 : GeneralizedHeytingAlgebra β]
  (a b : α × β), (bihimp a b).1 = bihimp a.1 b.1
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.ConnectedComponent.connectedComponentMk_eq_of_adj : ∀ {V : Type u} {G : SimpleGraph V} {v w : V}, G.Adj v w → G.connectedComponentMk v = G.connectedComponentMk w
-- Mathlib.AlgebraicGeometry.ColimitsOver
CategoryTheory.MorphismProperty.Over.mapComp.congr_simp : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] {P : CategoryTheory.MorphismProperty T}
  (Q : CategoryTheory.MorphismProperty T) [inst_1 : Q.IsMultiplicative] {X Y Z : T}
  [inst_2 : P.IsStableUnderComposition] {f : X ⟶ Y} (hf : P f) {g : Y ⟶ Z} (hg : P g) [inst_3 : Q.RespectsIso]
  (fg : X ⟶ Z) (hfg : fg = CategoryTheory.CategoryStruct.comp f g),
  CategoryTheory.MorphismProperty.Over.mapComp Q hf hg fg hfg =
    CategoryTheory.MorphismProperty.Over.mapComp Q hf hg fg hfg
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.Poly.denote_cons : ∀ (ctx : Nat.Internal.Linear.Context) (k : ℕ) (v : Nat.Internal.Linear.Var) (p : Nat.Internal.Linear.Poly),
  Nat.Internal.Linear.Poly.denote ctx ((k, v) :: p) =
    k * Nat.Internal.Linear.Var.denote ctx v + Nat.Internal.Linear.Poly.denote ctx p
-- Init.Data.SInt.Lemmas
instCommutativeInt32HMul : Std.Commutative fun x1 x2 => x1 * x2
-- Mathlib.Data.FunLike.Group
FunLike.addSemigroup.eq_1 : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : Add F] [inst_2 : AddSemigroup β]
  [inst_3 : IsAddApply F α β], FunLike.addSemigroup = Function.Injective.addSemigroup (fun f => ⇑f) ⋯ ⋯
-- Mathlib.Topology.MetricSpace.Gluing
Metric.Sum.mem_uniformity_iff_glueDist : ∀ {X : Type u} {Y : Type v} {Z : Type w} [inst : MetricSpace X] [inst_1 : MetricSpace Y] {Φ : Z → X} {Ψ : Z → Y}
  {ε : ℝ},
  0 < ε →
    ∀ (s : Set ((X ⊕ Y) × (X ⊕ Y))),
      s ∈ uniformity (X ⊕ Y) ↔ ∃ δ > 0, ∀ (a b : X ⊕ Y), Metric.glueDist Φ Ψ ε a b < δ → (a, b) ∈ s
-- Mathlib.Algebra.Group.TransferInstance
/-- Transfer `Neg` across an `Equiv`  -/
Equiv.Neg : {α : Type u_2} → {β : Type u_3} → α ≃ β → [Neg β] → Neg α
-- Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives
/-- If `p : X ⟶ Y` is a monomorphism that is not an isomorphism, there exists
a subobject `X'` of `Y` containing `X` (but different from `X`) such that
the inclusion `X ⟶ X'` is a pushout of a monomorphism in the family
`generatingMonomorphisms G`.  -/
CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.exists_pushouts : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {G : C} [CategoryTheory.Abelian C],
  CategoryTheory.IsSeparator G →
    ∀ {X Y : C} (p : X ⟶ Y) [CategoryTheory.Mono p],
      ¬CategoryTheory.IsIso p →
        ∃ X' i p',
          ∃ (_ : (CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms G).pushouts i) (_ :
            ¬CategoryTheory.IsIso i) (_ : CategoryTheory.Mono p'), CategoryTheory.CategoryStruct.comp i p' = p
-- Lean.Elab.MutualInductive
/-- `u ≤ ?r + rOffset`  -/
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.accLevel.go : Lean.Level →
  Array Lean.LMVarId → Lean.Level → ℤ → ExceptT Lean.MessageData (StateT Lean.Elab.Command.AccLevelState✝ Id) Unit
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.associator_naturality_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X X' : C}
  (f : X ⟶ X') (Y Z : C),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Y) Z)
      (CategoryTheory.MonoidalCategoryStruct.associator X' Y Z).hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight f (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z))
-- Mathlib.Analysis.Normed.Module.DoubleDual
NormedSpace.inclusionInDoubleDualWeak_apply : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] (X : Type u_2) [inst_1 : SeminormedAddCommGroup X]
  [inst_2 : NormedSpace 𝕜 X] (x : WeakSpace 𝕜 X),
  (NormedSpace.inclusionInDoubleDualWeak 𝕜 X) x =
    StrongDual.toWeakDual ((NormedSpace.inclusionInDoubleDual 𝕜 X) ((toWeakSpace 𝕜 X).symm x))
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.toList_filterMap : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} {γ : α → Type w}
  {f : (a : α) → β a → Option (γ a)},
  (Std.DTreeMap.filterMap f t).toList =
    List.filterMap (fun p => Option.map (fun x => ⟨p.fst, x⟩) (f p.fst p.snd)) t.toList
-- Lean.AuxRecursor
Lean.isBRecOnRecursor : Lean.Environment → Lean.Name → Bool
-- Mathlib.Topology.MetricSpace.Gluing
Metric.Sum.dist.eq_2 : ∀ {X : Type u} {Y : Type v} [inst : MetricSpace X] [inst_1 : MetricSpace Y] (x_2 y : Y),
  Metric.Sum.dist (Sum.inr x_2) (Sum.inr y) = dist x_2 y
-- Mathlib.GroupTheory.Coprod.Basic
Monoid.Coprod.inr.eq_1 : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N],
  Monoid.Coprod.inr = { toFun := fun x => Monoid.Coprod.mk (FreeMonoid.of (Sum.inr x)), map_one' := ⋯, map_mul' := ⋯ }
-- Mathlib.Topology.Bornology.Basic
Bornology.sUnion_bounded_univ : ∀ {α : Type u_2} {x : Bornology α}, ⋃₀ {s | Bornology.IsBounded s} = Set.univ
-- Mathlib.AlgebraicGeometry.StructureSheaf
_private.Mathlib.AlgebraicGeometry.StructureSheaf.0.AlgebraicGeometry.StructureSheaf.openToLocalizationₗ.congr_simp : ∀ (R M : Type u) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)) (x : ↑(AlgebraicGeometry.PrimeSpectrum.Top R))
  (hx : x ∈ U),
  AlgebraicGeometry.StructureSheaf.openToLocalizationₗ✝ R M U x hx =
    AlgebraicGeometry.StructureSheaf.openToLocalizationₗ✝ R M U x hx
-- Mathlib.LinearAlgebra.Matrix.Nonsingular
Matrix.nonsingular_iff_det_mem_nonZeroDivisors : ∀ {n : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] {R : Type u_4} [inst_2 : CommRing R] {A : Matrix n n R},
  A.Nonsingular ↔ A.det ∈ nonZeroDivisors R
-- Init.Data.Int.Linear
Int.Internal.Linear.orOver_cases : ∀ {n : ℕ} {p : ℕ → Prop}, Int.Internal.Linear.OrOver (n + 1) p → Int.Internal.Linear.OrOver_cases_type n p
-- Init.Data.Vector.OfFn
/-- Construct (in a monadic context) a vector by applying a monadic function to each index.  -/
Vector.ofFnM : {m : Type u_1 → Type u_2} → {α : Type u_1} → {n : ℕ} → [Monad m] → (Fin n → m α) → m (Vector α n)
-- Lean.Elab.DefView
Lean.Elab.instInhabitedDefKind : Inhabited Lean.Elab.DefKind
-- Lean.Environment
Lean.Kernel.Exception.invalidProj.injEq : ∀ (env : Lean.Kernel.Environment) (lctx : Lean.LocalContext) (proj : Lean.Expr) (env_1 : Lean.Kernel.Environment)
  (lctx_1 : Lean.LocalContext) (proj_1 : Lean.Expr),
  (Lean.Kernel.Exception.invalidProj env lctx proj = Lean.Kernel.Exception.invalidProj env_1 lctx_1 proj_1) =
    (env = env_1 ∧ lctx = lctx_1 ∧ proj = proj_1)
-- Aesop.Script.Step
Aesop.Script.Step.mk.inj : ∀ {preState : Lean.Meta.SavedState} {preGoal : Lean.MVarId} {tactic : Aesop.Script.Tactic}
  {postState : Lean.Meta.SavedState} {postGoals : Array Aesop.GoalWithMVars} {preState_1 : Lean.Meta.SavedState}
  {preGoal_1 : Lean.MVarId} {tactic_1 : Aesop.Script.Tactic} {postState_1 : Lean.Meta.SavedState}
  {postGoals_1 : Array Aesop.GoalWithMVars},
  { preState := preState, preGoal := preGoal, tactic := tactic, postState := postState, postGoals := postGoals } =
      { preState := preState_1, preGoal := preGoal_1, tactic := tactic_1, postState := postState_1,
        postGoals := postGoals_1 } →
    preState = preState_1 ∧ preGoal = preGoal_1 ∧ tactic = tactic_1 ∧ postState = postState_1 ∧ postGoals = postGoals_1
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SemanticTokensLegend.mk : Array String → Array String → Lean.Lsp.SemanticTokensLegend
-- Mathlib.CategoryTheory.Enriched.Limits.HasConicalLimits
/-- existence of conical limits (of shape) implies existence of limits (of shape)  -/
CategoryTheory.Enriched.HasConicalLimitsOfShape.hasLimitsOfShape : ∀ (J : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} J] (V : Type u') [inst_1 : CategoryTheory.Category.{v', u'} V]
  [inst_2 : CategoryTheory.MonoidalCategory V] (C : Type u) [inst_3 : CategoryTheory.Category.{v, u} C]
  [inst_4 : CategoryTheory.EnrichedOrdinaryCategory V C] [CategoryTheory.Enriched.HasConicalLimitsOfShape J V C],
  CategoryTheory.Limits.HasLimitsOfShape J C
-- Mathlib.Algebra.Ring.Hom.Defs
NonUnitalRingHom.instFunLike : {α : Type u_2} →
  {β : Type u_3} →
    [inst : NonUnitalNonAssocSemiring α] → [inst_1 : NonUnitalNonAssocSemiring β] → FunLike (α →ₙ+* β) α β
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
/-- The fork is in fact an equalizer.  -/
CategoryTheory.IsRegularMono.isLimit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y : C} →
      (f : X ⟶ Y) →
        [inst_1 : CategoryTheory.IsRegularMono f] → CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fork.ofι f ⋯)
-- Init.Data.Nat.ToString
_private.Init.Data.Nat.ToString.0.Nat.toDigitsCore_eq_toDigitsCore_nil_append : ∀ {b fuel n : ℕ} {cs₁ : List Char}, b.toDigitsCore fuel n cs₁ = b.toDigitsCore fuel n [] ++ cs₁
-- Mathlib.Analysis.Normed.Group.Seminorm
NonarchAddGroupNorm.toNonarchAddGroupSeminorm_eq_coe : ∀ {E : Type u_3} [inst : AddGroup E] {p : NonarchAddGroupNorm E}, ⇑p.toNonarchAddGroupSeminorm = ⇑p
-- Mathlib.MeasureTheory.Group.MeasurableEquiv
MeasurableEquiv.divLeft.eq_1 : ∀ {G : Type u_1} [inst : Group G] [inst_1 : MeasurableSpace G] [inst_2 : MeasurableMul G] [inst_3 : MeasurableInv G]
  (g : G), MeasurableEquiv.divLeft g = { toEquiv := Equiv.divLeft g, measurable_toFun := ⋯, measurable_invFun := ⋯ }