mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Combinatorics.Graph.Basic
Graph.mk.congr_simp : ∀ {α : Type u_3} {β : Type u_4} (vertexSet vertexSet_1 : Set α) (e_vertexSet : vertexSet = vertexSet_1)
  (IsLink IsLink_1 : β → α → α → Prop) (e_IsLink : IsLink = IsLink_1) (edgeSet edgeSet_1 : Set β)
  (e_edgeSet : edgeSet = edgeSet_1) (isLink_symm : ∀ ⦃e : β⦄, e ∈ edgeSet → Std.Symm (IsLink e))
  (eq_or_eq_of_isLink_of_isLink : ∀ ⦃e : β⦄ ⦃x y v w : α⦄, IsLink e x y → IsLink e v w → x = v ∨ x = w)
  (edge_mem_iff_exists_isLink : ∀ (e : β), e ∈ edgeSet ↔ ∃ x y, IsLink e x y)
  (left_mem_of_isLink : ∀ ⦃e : β⦄ ⦃x y : α⦄, IsLink e x y → x ∈ vertexSet),
  { vertexSet := vertexSet, IsLink := IsLink, edgeSet := edgeSet, isLink_symm := isLink_symm,
      eq_or_eq_of_isLink_of_isLink := eq_or_eq_of_isLink_of_isLink,
      edge_mem_iff_exists_isLink := edge_mem_iff_exists_isLink, left_mem_of_isLink := left_mem_of_isLink } =
    { vertexSet := vertexSet_1, IsLink := IsLink_1, edgeSet := edgeSet_1, isLink_symm := ⋯,
      eq_or_eq_of_isLink_of_isLink := ⋯, edge_mem_iff_exists_isLink := ⋯, left_mem_of_isLink := ⋯ }
-- Mathlib.Analysis.RCLike.Sqrt
Complex.sqrt_of_nonneg : ∀ {a : ℂ}, 0 ≤ a → a.sqrt = ↑√a.re
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
CategoryTheory.Oplax.StrongTrans.whiskerLeft_naturality_comp_assoc : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {G H : CategoryTheory.OplaxFunctor B C} (θ : CategoryTheory.Oplax.StrongTrans G H) {a b c : B} {a' : C}
  (f : a' ⟶ G.obj a) (g : a ⟶ b) (h : b ⟶ c) {Z : a' ⟶ H.obj c}
  (h_1 :
    CategoryTheory.CategoryStruct.comp f
        (CategoryTheory.CategoryStruct.comp (θ.app a) (CategoryTheory.CategoryStruct.comp (H.map g) (H.map h))) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerLeft f (θ.naturality (CategoryTheory.CategoryStruct.comp g h)).hom)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerLeft (θ.app a) (H.mapComp g h)))
        h_1) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerRight (G.mapComp g h) (θ.app c)))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerLeft f
          (CategoryTheory.Bicategory.associator (G.map g) (G.map h) (θ.app c)).hom)
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Bicategory.whiskerLeft f
            (CategoryTheory.Bicategory.whiskerLeft (G.map g) (θ.naturality h).hom))
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.Bicategory.whiskerLeft f
              (CategoryTheory.Bicategory.associator (G.map g) (θ.app b) (H.map h)).inv)
            (CategoryTheory.CategoryStruct.comp
              (CategoryTheory.Bicategory.whiskerLeft f
                (CategoryTheory.Bicategory.whiskerRight (θ.naturality g).hom (H.map h)))
              (CategoryTheory.CategoryStruct.comp
                (CategoryTheory.Bicategory.whiskerLeft f
                  (CategoryTheory.Bicategory.associator (θ.app a) (H.map g) (H.map h)).hom)
                h_1)))))
-- Mathlib.Algebra.BigOperators.Balance
Fintype.map_balance : ∀ {ι : Type u_1} {H : Type u_2} {F : Type u_3} {G : Type u_4} [inst : Fintype ι] [inst_1 : AddCommGroup G]
  [inst_2 : Module ℚ≥0 G] [inst_3 : AddCommGroup H] [inst_4 : Module ℚ≥0 H] [inst_5 : FunLike F G H]
  [LinearMapClass F ℚ≥0 G H] (g : F) (f : ι → G) (a : ι), g (Fintype.balance f a) = Fintype.balance (⇑g ∘ f) a
-- Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
AlgebraicGeometry.PresheafedSpace.GlueData.ιIsOpenImmersion : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (D : AlgebraicGeometry.PresheafedSpace.GlueData C)
  [inst_1 : CategoryTheory.Limits.HasLimits C] (i : D.J), AlgebraicGeometry.PresheafedSpace.IsOpenImmersion (D.ι i)
-- Mathlib.GroupTheory.Perm.MaximalSubgroups
/-- In the permutation group, the stabilizer of a set acts primitively on that set.  -/
Equiv.Perm.stabilizer_isPreprimitive : ∀ {α : Type u_2} (s : Set α), MulAction.IsPreprimitive ↥(MulAction.stabilizer (Equiv.Perm α) s) ↑s
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
NumberField.mixedEmbedding.fundamentalCone.torsion_smul_mem_of_mem : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] {x : NumberField.mixedEmbedding.mixedSpace K},
  x ∈ NumberField.mixedEmbedding.fundamentalCone K →
    ∀ {ζ : (NumberField.RingOfIntegers K)ˣ},
      ζ ∈ NumberField.Units.torsion K → ζ • x ∈ NumberField.mixedEmbedding.fundamentalCone K
-- Mathlib.RingTheory.MvPowerSeries.Substitution
/-- Substitution of power series into a power series

It coincides with evaluation when `f` is a polynomial, or under `HasSubst a`.
Otherwise, it is given the dummy value `0`.  -/
MvPowerSeries.subst : {σ : Type u_1} →
  {R : Type u_3} →
    [inst : CommRing R] →
      {τ : Type u_4} →
        {S : Type u_5} →
          [inst_1 : CommRing S] → [Algebra R S] → (σ → MvPowerSeries τ S) → MvPowerSeries σ R → MvPowerSeries τ S
-- Mathlib.CategoryTheory.Category.PartialFun
partialFunEquivPointed_counitIso_hom_app_toFun : ∀ (X : Pointed) (a : ((pointedToPartialFun.comp partialFunToPointed).obj X).X),
  (partialFunEquivPointed.counitIso.hom.app X).toFun a = (Equiv.optionSubtypeNe X.point) a
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
AffineSubspace.topEquiv_symm_apply_coe : ∀ (k : Type u_1) (V : Type u_2) (P : Type u_3) [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] (a : P), ↑((AffineSubspace.topEquiv k V P).symm a) = a
-- Init.Data.Array.Find
/-- `p` does not hold for elements with indices less than `xs.findIdx p`.  -/
Array.not_of_lt_findIdx : ∀ {α : Type u_1} {p : α → Bool} {xs : Array α} {i : ℕ} (h : i < Array.findIdx p xs), p xs[i] = false
-- Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
/-- Any category with pushouts and an initial object has a colimit cocone for each walking pair.  -/
colimitCoconeOfInitialAndPushouts : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Limits.HasInitial C] →
      [CategoryTheory.Limits.HasPushouts C] →
        (F : CategoryTheory.Functor (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) C) →
          CategoryTheory.Limits.ColimitCocone F
-- Std.Sat.AIG.CachedGatesLemmas
Std.Sat.AIG.mkXorCached_le_size : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] (aig : Std.Sat.AIG α) {input : aig.BinaryInput},
  aig.decls.size ≤ (aig.mkXorCached input).aig.decls.size
-- Mathlib.Analysis.Complex.Basic
Complex.inv_eq_conj : ∀ {z : ℂ}, ‖z‖ = 1 → z⁻¹ = (starRingEnd ℂ) z
-- Mathlib.Topology.UniformSpace.Equiv
UniformEquiv.preimage_symm : ∀ {α : Type u} {β : Type u_1} [inst : UniformSpace α] [inst_1 : UniformSpace β] (h : α ≃ᵤ β),
  Set.preimage ⇑h.symm = Set.image ⇑h
-- Mathlib.Order.Comparable
LT.lt.not_incompRel : ∀ {α : Type u_1} {a b : α} [inst : Preorder α], a < b → ¬IncompRel (fun x1 x2 => x1 ≤ x2) a b
-- Mathlib.Order.Hom.Basic
OrderEmbedding.subtype_injective : ∀ {α : Type u_2} [inst : Preorder α] (p : α → Prop), Function.Injective ⇑(OrderEmbedding.subtype p)
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.monoCLM_eq_zero : ∀ (𝕜 : Type u_1) {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : SMulCommClass ℝ 𝕜 F] {n₁ n₂ : ℕ∞} {K₁ K₂ : TopologicalSpace.Compacts E},
  ¬(n₂ ≤ n₁ ∧ K₁ ≤ K₂) → ContDiffMapSupportedIn.monoCLM 𝕜 = 0
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
/-- Let `C(G, A)` denote the complex of inhomogeneous chains of `A : Rep k G`. This lemma
says `d₁₀` gives a simpler expression for the 0th differential: that is, the following
square commutes:
```
  C₁(G, A) --d 1 0--> C₀(G, A)
    |                   |
    |                   |
    |                   |
    v                   v
  (G →₀ A) ----d₁₀----> A
```
where the vertical arrows are `chainsIso₁` and `chainsIso₀` respectively.
 -/
groupHomology.comp_d₁₀_eq : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G),
  CategoryTheory.CategoryStruct.comp (groupHomology.chainsIso₁ A).hom (groupHomology.d₁₀ A) =
    CategoryTheory.CategoryStruct.comp ((groupHomology.inhomogeneousChains A).d 1 0) (groupHomology.chainsIso₀ A).hom
-- Mathlib.Computability.TuringMachine.StackTuringMachine
_private.Mathlib.Computability.TuringMachine.StackTuringMachine.0.Turing.TM2to1.trStmts₁.match_1.eq_2 : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} (motive : Turing.TM2.Stmt Γ Λ σ → Sort u_5) (k : K)
  (f : σ → Option (Γ k) → σ) (q : Turing.TM2.Stmt Γ Λ σ)
  (h_1 : (k : K) → (f : σ → Γ k) → (q : Turing.TM2.Stmt Γ Λ σ) → motive (Turing.TM2.Stmt.push k f q))
  (h_2 : (k : K) → (f : σ → Option (Γ k) → σ) → (q : Turing.TM2.Stmt Γ Λ σ) → motive (Turing.TM2.Stmt.peek k f q))
  (h_3 : (k : K) → (f : σ → Option (Γ k) → σ) → (q : Turing.TM2.Stmt Γ Λ σ) → motive (Turing.TM2.Stmt.pop k f q))
  (h_4 : (a : σ → σ) → (q : Turing.TM2.Stmt Γ Λ σ) → motive (Turing.TM2.Stmt.load a q))
  (h_5 : (a : σ → Bool) → (q₁ q₂ : Turing.TM2.Stmt Γ Λ σ) → motive (Turing.TM2.Stmt.branch a q₁ q₂))
  (h_6 : (x : Turing.TM2.Stmt Γ Λ σ) → motive x),
  (match Turing.TM2.Stmt.peek k f q with
    | Turing.TM2.Stmt.push k f q => h_1 k f q
    | Turing.TM2.Stmt.peek k f q => h_2 k f q
    | Turing.TM2.Stmt.pop k f q => h_3 k f q
    | Turing.TM2.Stmt.load a q => h_4 a q
    | Turing.TM2.Stmt.branch a q₁ q₂ => h_5 a q₁ q₂
    | x => h_6 x) =
    h_2 k f q
-- Init.Conv
/-- `· conv` focuses on the main conv goal and tries to solve it using `s`.  -/
Lean.Parser.Tactic.Conv.«conv·_» : Lean.ParserDescr
-- Mathlib.RingTheory.Radical.Basic
UniqueFactorizationMonoid.primeFactors_pow : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] [inst_1 : NormalizationMonoid M] [inst_2 : UniqueFactorizationMonoid M]
  (a : M) {n : ℕ}, n ≠ 0 → UniqueFactorizationMonoid.primeFactors (a ^ n) = UniqueFactorizationMonoid.primeFactors a
-- Mathlib.Analysis.InnerProductSpace.Orthogonal
ClosedSubmodule.sub_mem_orthogonal_of_inner_right : ∀ {𝕜 : Type u_4} {E : Type u_5} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {K : ClosedSubmodule 𝕜 E} {x y : E}, (∀ (v : ↥K), inner 𝕜 (↑v) x = inner 𝕜 (↑v) y) → x - y ∈ Kᗮ
-- Mathlib.CategoryTheory.Abelian.Refinements
CategoryTheory.ShortComplex.comp_homologyπ_eq_iff_up_to_refinements : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {S : CategoryTheory.ShortComplex C} {A : C} (z₂ z₂' : A ⟶ S.cycles),
  CategoryTheory.CategoryStruct.comp z₂ S.homologyπ = CategoryTheory.CategoryStruct.comp z₂' S.homologyπ ↔
    ∃ A' π,
      ∃ (_ : CategoryTheory.Epi π),
        ∃ x₁,
          CategoryTheory.CategoryStruct.comp π z₂ =
            CategoryTheory.CategoryStruct.comp π z₂' + CategoryTheory.CategoryStruct.comp x₁ S.toCycles
-- Mathlib.Data.ZMod.QuotientGroup
MulAction.orbitZPowersEquiv_symm_apply : ∀ {α : Type u_3} {β : Type u_4} [inst : Group α] (a : α) [inst_1 : MulAction α β] (b : β)
  (k : ZMod (Function.minimalPeriod (fun x => a • x) b)),
  (MulAction.orbitZPowersEquiv a b).symm k = ⟨a, ⋯⟩ ^ k.cast • ⟨b, ⋯⟩
-- Init.PropLemmas
forall_congr' : ∀ {α : Sort u_1} {p q : α → Prop}, (∀ (a : α), p a ↔ q a) → ((∀ (a : α), p a) ↔ ∀ (a : α), q a)
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
/-- If every `x ∈ s` has a neighbourhood within `s` on which `b ↦ ∏' i, f i b` converges uniformly,
then the product converges locally uniformly on `s`. Note that this is not a tautology, and the
converse is only true if the domain is locally compact.  -/
multipliableLocallyUniformlyOn_of_of_forall_exists_nhds : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : CommMonoid α] {f : ι → β → α} {s : Set β}
  [inst_1 : UniformSpace α] [inst_2 : TopologicalSpace β],
  (∀ x ∈ s, ∃ t ∈ nhdsWithin x s, MultipliableUniformlyOn f t) → MultipliableLocallyUniformlyOn f s
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
/-- Equivalences between measurable spaces. Main application is the simplification of measurability
statements along measurable equivalences.  -/
«term_≃ᵐ_» : Lean.TrailingParserDescr
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Arg.erased : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.Arg pu
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.union_left : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ t₃ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → t₃.WF → t₁.Equiv t₂ → (t₁ ∪ t₃).Equiv (t₂ ∪ t₃)
-- Lean.Elab.PreDefinition.Structural.Eqns
_private.Lean.Elab.PreDefinition.Structural.Eqns.0.Lean.Elab.Structural.getUnfoldFor? : Lean.Name → Lean.MetaM (Option Lean.Name)
-- Mathlib.RingTheory.LocalRing.Pullback
RingHom.map_pullbackSnd_ker_pullbackFst_eq : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : Ring R] [inst_1 : Ring S] [inst_2 : Semiring T] (f : R →+* T)
  (g : S →+* T), Ideal.map (f.pullbackSnd g) (RingHom.ker (f.pullbackFst g)) = RingHom.ker g
-- Std.Data.Iterators.Lemmas.Combinators.TakeWhile
Std.Iter.toArray_takeWhile_of_finite : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] {P : β → Bool} [Std.Iterators.Finite α Id] {it : Std.Iter β},
  (Std.Iter.takeWhile P it).toArray = Array.takeWhile P it.toArray
-- Lean.Elab.BuiltinTerm
Lean.Elab.Term.elabIncludeStr : Lean.Elab.Term.TermElab
-- Mathlib.GroupTheory.Congruence.Basic
AddCon.comap_addConGen_equiv : ∀ {M : Type u_4} {N : Type u_5} [inst : Add M] [inst_1 : Add N] (f : M ≃+ N) (rel : N → N → Prop),
  AddCon.comap ⇑f ⋯ (addConGen rel) = addConGen fun x y => rel (f x) (f y)
-- Std.Data.DTreeMap.Raw.Basic
/-- Returns the `n`-th smallest key, or `none` if `n` is at least `t.size`.  -/
Std.DTreeMap.Raw.keyAtIdx? : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → Std.DTreeMap.Raw α β cmp → ℕ → Option α
-- Mathlib.Algebra.Order.Pi
Pi.mulSingle_le_one : ∀ {ι : Type u_6} {α : ι → Type u_7} [inst : DecidableEq ι] [inst_1 : (i : ι) → One (α i)]
  [inst_2 : (i : ι) → Preorder (α i)] {i : ι} {a : α i}, Pi.mulSingle i a ≤ 1 ↔ a ≤ 1
-- Mathlib.Topology.Algebra.Module.EmbeddingOfLocal
/-- Consider a vector space `E` over a `NontriviallyNormedField` `𝕜`, and `t₁`, `t₂` two topologies
on `E` which are compatible with the vector space structure.

Assume that there is a `t₁`-neighborhood of zero `V` such that the two topogies induce the
same topology *on the subspace `V`*. Then `t₁ = t₂`.  -/
ContinuousSMul.topology_eq_of_induced_eq : ∀ (𝕜₁ : Type u_1) {E : Type u_3} [inst : NontriviallyNormedField 𝕜₁] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜₁ E]
  (t₁ t₂ : TopologicalSpace E) [IsTopologicalAddGroup E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜₁ E]
  [ContinuousSMul 𝕜₁ E] {V : Set E},
  V ∈ nhds 0 → TopologicalSpace.induced Subtype.val t₁ = TopologicalSpace.induced Subtype.val t₂ → t₁ = t₂
-- Mathlib.CategoryTheory.Preadditive.Yoneda.Basic
/-- The Yoneda embedding for preadditive categories sends an object `X` to the copresheaf sending an
object `Y` to the group of morphisms `X ⟶ Y`. At each point, we get an additional `End X`-module
structure, see `preadditiveCoyonedaObj`.
 -/
CategoryTheory.preadditiveCoyoneda : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Preadditive C] → CategoryTheory.Functor Cᵒᵖ (CategoryTheory.Functor C AddCommGrpCat)
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.Hom.comm_to_apply : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {C₁ C₂ : HomologicalComplex V c}
  (f : C₁.Hom C₂) (j : ι) {F : V → V → Type uF} {carrier : V → Type w}
  {instFunLike : (X Y : V) → FunLike (F X Y) (carrier X) (carrier Y)} [inst_2 : CategoryTheory.ConcreteCategory V F]
  (x : carrier (C₁.xPrev j)),
  (CategoryTheory.ConcreteCategory.hom (C₂.dTo j)) ((CategoryTheory.ConcreteCategory.hom (f.prev j)) x) =
    (CategoryTheory.ConcreteCategory.hom (f.f j)) ((CategoryTheory.ConcreteCategory.hom (C₁.dTo j)) x)
-- Mathlib.Probability.Kernel.Composition.CompProd
ProbabilityTheory.Kernel.compProd_restrict : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} {κ : ProbabilityTheory.Kernel α β} [ProbabilityTheory.IsSFiniteKernel κ]
  {η : ProbabilityTheory.Kernel (α × β) γ} [ProbabilityTheory.IsSFiniteKernel η] {s : Set β} {t : Set γ}
  (hs : MeasurableSet s) (ht : MeasurableSet t), (κ.restrict hs).compProd (η.restrict ht) = (κ.compProd η).restrict ⋯
-- Mathlib.Topology.Compactness.CountablyCompact
/-- A compact set is countably compact.  -/
IsCompact.isCountablyCompact : ∀ {E : Type u_2} [inst : TopologicalSpace E] {A : Set E}, IsCompact A → IsCountablyCompact A
-- Mathlib.SetTheory.Cardinal.Regular
Cardinal.isRegular_lift_iff : ∀ {κ : Cardinal.{v}}, (Cardinal.lift.{u, v} κ).IsRegular ↔ κ.IsRegular
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SymbolKind.object.sizeOf_spec : sizeOf Lean.Lsp.SymbolKind.object = 1
-- Mathlib.Algebra.Order.Group.Multiset
Multiset.addHom_ext : ∀ {α : Type u_1} {β : Type u_2} [inst : AddZeroClass β] ⦃f g : Multiset α →+ β⦄, (∀ (x : α), f {x} = g {x}) → f = g
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.BinaryBicone.binary_cofan_inl_toCocone : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {P Q : C} (c : CategoryTheory.Limits.BinaryBicone P Q), CategoryTheory.Limits.BinaryCofan.inl c.toCocone = c.inl
-- Mathlib.CategoryTheory.Groupoid.FreeGroupoid
Quiver.FreeGroupoid.congr_comp_reverse : ∀ {V : Type u} [inst : Quiver V] {X Y : CategoryTheory.Paths (Quiver.Symmetrify V)} (p : X ⟶ Y),
  Quot.mk (CategoryTheory.HomRel.CompClosure Quiver.FreeGroupoid.redStep)
      (CategoryTheory.CategoryStruct.comp p (Quiver.Path.reverse p)) =
    Quot.mk (CategoryTheory.HomRel.CompClosure Quiver.FreeGroupoid.redStep) (CategoryTheory.CategoryStruct.id X)
-- Batteries.Logic
eqRec_heq_self : ∀ {α : Sort u_1} {a : α} {motive : (a' : α) → a = a' → Sort u_2} (x : motive a ⋯) {a' : α} (e : a = a'), e ▸ x ≍ x
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.isSome_getKey?_iff_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {a : α},
  (t.getKey? a).isSome = true ↔ a ∈ t
-- Mathlib.Data.Finset.Filter
Finset.filter_subset_filter : ∀ {α : Type u_1} (p : α → Prop) [inst : DecidablePred p] {s t : Finset α}, s ⊆ t → Finset.filter p s ⊆ Finset.filter p t
-- Mathlib.NumberTheory.ModularForms.Basic
ModularForm.coe_intCast : ∀ {Γ : Subgroup (GL (Fin 2) ℝ)} [inst : Γ.HasDetPlusMinusOne] (z : ℤ), ⇑↑z = ↑z
-- Mathlib.CategoryTheory.Category.Pointed
Pointed.instCoeSortType : CoeSort Pointed (Type u_1)
-- Lean.Server.InfoUtils
Lean.Elab.HoverableInfoPrio.isPartialTermInfo : Lean.Elab.HoverableInfoPrio → Bool
-- Lean.DocString.Markdown
/-- Builtin inline renderers, for bootstrapping.  -/
_private.Lean.DocString.Markdown.0.Lean.Doc.builtinInlineMdRenderers : IO.Ref (Lean.NameMap Lean.Doc.InlineMdRenderer)
-- Aesop.Index.Forward
/-- Get the forward rule with the given rule name.  -/
Aesop.ForwardIndex.getRuleWithName? : Aesop.RuleName → Aesop.ForwardIndex → Option Aesop.ForwardRule
-- Mathlib.Algebra.Order.Sub.Unbundled.Basic
AddLECancellable.lt_tsub_iff_right_of_le : ∀ {α : Type u_1} [inst : AddCommSemigroup α] [inst_1 : PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α]
  [inst_4 : Sub α] [OrderedSub α] {a b c : α}, AddLECancellable c → c ≤ b → (a < b - c ↔ a + c < b)
-- Init.Data.Vector.Lex
Vector.not_le : ∀ {α : Type u_1} {n : ℕ} [inst : LT α] {xs ys : Vector α n}, ¬xs ≤ ys ↔ ys < xs
-- Mathlib.Topology.Algebra.ProperAction.Basic
/-- A group `G` acts properly on a T2 topological space `X` if and only if for all ultrafilters
`𝒰` on `X × G`, if `𝒰` converges to `(x₁, x₂)` along the map `(g, x) ↦ (g • x, x)`,
then there exists `g : G` such that `𝒰.fst` converges to `g`.  -/
properSMul_iff_continuousSMul_ultrafilter_tendsto_t2 : ∀ {G : Type u_1} {X : Type u_2} [inst : Group G] [inst_1 : MulAction G X] [inst_2 : TopologicalSpace G]
  [inst_3 : TopologicalSpace X] [T2Space X],
  ProperSMul G X ↔
    ContinuousSMul G X ∧
      ∀ (𝒰 : Ultrafilter (G × X)) (x₁ x₂ : X),
        Filter.Tendsto (fun gx => (gx.1 • gx.2, gx.2)) (↑𝒰) (nhds (x₁, x₂)) → ∃ g, Filter.Tendsto Prod.fst (↑𝒰) (nhds g)
-- Mathlib.RingTheory.Finiteness.Basic
RingHom.Finite.comp : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : CommRing C]
  {g : B →+* C} {f : A →+* B}, g.Finite → f.Finite → (g.comp f).Finite
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getElem!_alter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k k' : α}
  [inst_1 : Inhabited β] {f : Option β → Option β},
  (t.alter k f)[k']! = if cmp k k' = Ordering.eq then (f t[k]?).get! else t[k']!
-- Mathlib.Algebra.Group.Basic
add_eq_zero_iff_neg_eq : ∀ {G : Type u_3} [inst : AddGroup G] {a b : G}, a + b = 0 ↔ -a = b
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F : Cᵒᵖ ⥤ D` reflects colimits, then `F.rightOp : C ⥤ Dᵒᵖ` reflects limits.  -/
CategoryTheory.Limits.reflectsLimits_rightOp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor Cᵒᵖ D) [CategoryTheory.Limits.ReflectsColimits F],
  CategoryTheory.Limits.ReflectsLimits F.rightOp
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get_union_of_not_mem_right : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {m₁ m₂ : Std.DTreeMap.Raw α (fun x => β) cmp}
  [inst : Std.TransCmp cmp] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} (not_mem : k ∉ m₂) {h' : k ∈ m₁ ∪ m₂},
  Std.DTreeMap.Raw.Const.get (m₁ ∪ m₂) k h' = Std.DTreeMap.Raw.Const.get m₁ k ⋯
-- Mathlib.LinearAlgebra.Multilinear.TensorProduct
/-- A more bundled version of `MultilinearMap.domCoprod` that maps
`((ι₁ → N) → N₁) ⊗ ((ι₂ → N) → N₂)` to `(ι₁ ⊕ ι₂ → N) → N₁ ⊗ N₂`.  -/
MultilinearMap.domCoprod' : {R : Type u_1} →
  {ι₁ : Type u_2} →
    {ι₂ : Type u_3} →
      [inst : CommSemiring R] →
        {N₁ : Type u_6} →
          [inst_1 : AddCommMonoid N₁] →
            [inst_2 : Module R N₁] →
              {N₂ : Type u_7} →
                [inst_3 : AddCommMonoid N₂] →
                  [inst_4 : Module R N₂] →
                    {N : Type u_8} →
                      [inst_5 : AddCommMonoid N] →
                        [inst_6 : Module R N] →
                          TensorProduct R (MultilinearMap R (fun x => N) N₁) (MultilinearMap R (fun x => N) N₂) →ₗ[R]
                            MultilinearMap R (fun x => N) (TensorProduct R N₁ N₂)
-- Mathlib.Algebra.Order.Hom.Monoid
/-- Makes an ordered additive group homomorphism from a proof that the map preserves
addition.  -/
OrderAddMonoidHom.mk' : {α : Type u_2} →
  {β : Type u_3} →
    {x : AddCommGroup α} →
      {x_1 : Preorder α} →
        {x_2 : AddCommGroup β} →
          {x_3 : PartialOrder β} → (f : α → β) → Monotone f → (∀ (a b : α), f (a + b) = f a + f b) → α →+o β
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.Mor₂.isoHom.injEq : ∀ (e : Lean.Expr) (isoLift : Mathlib.Tactic.BicategoryLike.IsoLift) (iso : Mathlib.Tactic.BicategoryLike.Mor₂Iso)
  (e_1 : Lean.Expr) (isoLift_1 : Mathlib.Tactic.BicategoryLike.IsoLift) (iso_1 : Mathlib.Tactic.BicategoryLike.Mor₂Iso),
  (Mathlib.Tactic.BicategoryLike.Mor₂.isoHom e isoLift iso =
      Mathlib.Tactic.BicategoryLike.Mor₂.isoHom e_1 isoLift_1 iso_1) =
    (e = e_1 ∧ isoLift = isoLift_1 ∧ iso = iso_1)
-- Std.Data.DTreeMap.Internal.Model
/-- Model implementation of the `alter` function.
Internal implementation detail of the tree map
 -/
Std.DTreeMap.Internal.Impl.alterₘ : {α : Type u} →
  {β : α → Type v} →
    [inst : Ord α] →
      [Std.OrientedOrd α] →
        [Std.LawfulEqOrd α] →
          (k : α) →
            (Option (β k) → Option (β k)) →
              (t : Std.DTreeMap.Internal.Impl α β) → t.Balanced → Std.DTreeMap.Internal.Impl α β