mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.beq_eq_beqModel : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] [inst_2 : Hashable α]
  [inst_3 : (k : α) → BEq (β k)] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β},
  Std.DHashMap.Internal.Raw.WFImp ↑m₁ →
    Std.DHashMap.Internal.Raw.WFImp ↑m₂ →
      m₁.beq m₂ =
        Std.Internal.List.beqModel (Std.DHashMap.Internal.toListModel (↑m₁).buckets)
          (Std.DHashMap.Internal.toListModel (↑m₂).buckets)
-- Mathlib.Topology.Algebra.Ring.Basic
Subsemiring.semitopologicalSemiring : ∀ {R : Type u_1} [inst : TopologicalSpace R] [inst_1 : Semiring R] [IsSemitopologicalSemiring R] (S : Subsemiring R),
  IsSemitopologicalSemiring ↥S
-- Mathlib.Algebra.Group.Hom.Defs
ZeroHom.cancel_right : ∀ {M : Type u_4} {N : Type u_5} {P : Type u_6} [inst : Zero M] [inst_1 : Zero N] [inst_2 : Zero P] {g₁ g₂ : ZeroHom N P}
  {f : ZeroHom M N}, Function.Surjective ⇑f → (g₁.comp f = g₂.comp f ↔ g₁ = g₂)
-- Mathlib.Tactic.TermCongr
Mathlib.Tactic.TermCongr.CongrResult.mk.sizeOf_spec : ∀ (lhs rhs : Lean.Expr) (pf? : Option (Mathlib.Tactic.TermCongr.CongrType → Lean.MetaM Lean.Expr)),
  sizeOf { lhs := lhs, rhs := rhs, pf? := pf? } = 1 + sizeOf lhs + sizeOf rhs + sizeOf pf?
-- Mathlib.CategoryTheory.Bicategory.Modification.Lax
CategoryTheory.Lax.OplaxTrans.Hom.of.sizeOf_spec : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.LaxFunctor B C} {η θ : F ⟶ G} [inst_2 : SizeOf B] [inst_3 : SizeOf C]
  (as : CategoryTheory.Lax.OplaxTrans.Modification η θ), sizeOf { as := as } = 1 + sizeOf as
-- Mathlib.Combinatorics.Additive.ETransform
Finset.mulDysonETransform.eq_1 : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : CommGroup α] (e : α) (x : Finset α × Finset α),
  Finset.mulDysonETransform e x = (x.1 ∪ e • x.2, x.2 ∩ e⁻¹ • x.1)
-- Mathlib.Algebra.Order.Positive.Ring
Positive.addRightCancelSemigroup : {M : Type u_3} →
  [inst : AddRightCancelMonoid M] →
    [inst_1 : Preorder M] → [AddLeftStrictMono M] → AddRightCancelSemigroup { x // 0 < x }
-- Mathlib.Topology.Order.LeftRight
IsAntichain.interior_eq_empty : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : Preorder α] [∀ (x : α), (nhdsWithin x (Set.Iio x)).NeBot]
  {s : Set α}, IsAntichain (fun x1 x2 => x1 ≤ x2) s → interior s = ∅
-- Mathlib.Analysis.Normed.Group.Basic
enorm_mul₃_le' : ∀ {E : Type u_8} [inst : TopologicalSpace E] [inst_1 : ESeminormedMonoid E] {a b c : E},
  ‖a * b * c‖ₑ ≤ ‖a‖ₑ + ‖b‖ₑ + ‖c‖ₑ
-- Mathlib.RingTheory.WittVector.Defs
WittVector.instNeg : {p : ℕ} → {R : Type u_1} → [hp : Fact (Nat.Prime p)] → [CommRing R] → Neg (WittVector p R)
-- Mathlib.Data.Finset.Lattice.Fold
Finset.inf_le_of_le : ∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeInf α] [inst_1 : OrderTop α] {s : Finset β} {f : β → α} {a : α}
  {b : β}, b ∈ s → f b ≤ a → s.inf f ≤ a
-- Init.Grind.Ordered.Field
Lean.Grind.Field.IsOrdered.inv_nonpos_iff : ∀ {R : Type u} [inst : Lean.Grind.Field R] [inst_1 : LE R] [inst_2 : LT R] [Std.LawfulOrderLT R]
  [inst_4 : Std.IsLinearOrder R] [Lean.Grind.OrderedRing R] {a : R}, a⁻¹ ≤ 0 ↔ a ≤ 0
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.isValidLe : Int.Internal.Linear.Poly → Bool
-- Init.Data.Nat.Bitwise.Lemmas
Nat.instAssociativeHXor : Std.Associative fun x1 x2 => x1 ^^^ x2
-- Mathlib.Algebra.QuadraticAlgebra.Basic
QuadraticAlgebra.trace_intCast : ∀ {R : Type u_2} {a b : R} [inst : CommRing R] (n : ℤ), QuadraticAlgebra.trace ↑n = 2 * ↑n
-- Mathlib.CategoryTheory.Functor.OfSequence
/-- The morphism `X i ⟶ X j` obtained by composing morphisms of
the form `X n ⟶ X (n + 1)` when `i ≤ j`.  -/
CategoryTheory.Functor.OfSequence.map : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {X : ℕ → C} → ((n : ℕ) → X n ⟶ X (n + 1)) → (i j : ℕ) → i ≤ j → (X i ⟶ X j)
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
/-- Construct an adjoint equivalence from 2-isomorphisms by upgrading `ε` to a counit.  -/
CategoryTheory.Bicategory.Equivalence.mkOfAdjointifyCounit : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {a b : B} →
      {f : a ⟶ b} →
        {g : b ⟶ a} →
          (CategoryTheory.CategoryStruct.id a ≅ CategoryTheory.CategoryStruct.comp f g) →
            (CategoryTheory.CategoryStruct.comp g f ≅ CategoryTheory.CategoryStruct.id b) →
              CategoryTheory.Bicategory.Equivalence a b
-- Mathlib.Data.Seq.Computation
Computation.Results.val_unique : ∀ {α : Type u} {s : Computation α} {a b : α} {m n : ℕ}, s.Results a m → s.Results b n → a = b
-- Mathlib.LinearAlgebra.ExteriorPower.Basic
/-- If a family of vectors spans `M`, then the family of its `n`-fold exterior products spans
`⋀[R]^n M`. This is a variant of `ιMulti_family_span_fixedDegree_of_span` where we
work in the exterior power and not the exterior algebra.  -/
exteriorPower.ιMulti_family_span_of_span : ∀ (R : Type u) [inst : CommRing R] {n : ℕ} {M : Type u_1} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {I : Type u_4}
  [inst_3 : LinearOrder I] {v : I → M},
  Submodule.span R (Set.range v) = ⊤ → Submodule.span R (Set.range (exteriorPower.ιMulti_family R n v)) = ⊤
-- Mathlib.Combinatorics.Enumerative.Composition
/-- The length of a composition, i.e., the number of blocks in the composition.  -/
Composition.length : {n : ℕ} → Composition n → ℕ
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.Formatter.formatterAliasesRef : IO.Ref (Lean.NameMap Lean.PrettyPrinter.Formatter.FormatterAliasValue)
-- Mathlib.RingTheory.Extension.Presentation.Core
Algebra.Presentation.HasCoeffs.coeffs_relation_mem_range : ∀ {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] {P : Algebra.Presentation R S ι σ} (R₀ : Type u_5) [inst_3 : CommRing R₀]
  [inst_4 : Algebra R₀ R] [inst_5 : Algebra R₀ S] [inst_6 : IsScalarTower R₀ R S] [P.HasCoeffs R₀] (x : σ),
  ↑(MvPolynomial.coeffs (P.relation x)) ⊆ Set.range ⇑(algebraMap R₀ R)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.le_minKey? : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  (∀ (k' : α), t.minKey? = some k' → (cmp k k').isLE = true) ↔ ∀ k' ∈ t, (cmp k k').isLE = true
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.isoCocycles₂_inv_comp_iCocycles_apply : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) (x : ↥(groupCohomology.cocycles₂ A)),
  (CategoryTheory.ConcreteCategory.hom (groupCohomology.iCocycles A 2))
      ((CategoryTheory.ConcreteCategory.hom (groupCohomology.isoCocycles₂ A).inv) x) =
    (CategoryTheory.ConcreteCategory.hom
        (CategoryTheory.CategoryStruct.comp (groupCohomology.shortComplexH2 A).moduleCatLeftHomologyData.i
          (groupCohomology.cochainsIso₂ A).inv))
      x
-- Std.Data.Internal.List.Associative
Std.Internal.List.DistinctKeys.filter : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {l : List ((a : α) × β a)} {f : (a : α) → β a → Bool},
  Std.Internal.List.DistinctKeys l → Std.Internal.List.DistinctKeys (List.filter (fun p => f p.fst p.snd) l)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
_private.Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting.0.CategoryTheory.Limits.termY₃_1 : Lean.ParserDescr
-- Mathlib.Order.UpperLower.CompleteLattice
UpperSet.map.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (f : α ≃o β),
  UpperSet.map f =
    { toFun := fun s => { carrier := ⇑f '' ↑s, upper' := ⋯ }, invFun := fun t => { carrier := ⇑f ⁻¹' ↑t, upper' := ⋯ },
      left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.aleph0_add_ofNat : ∀ {n : ℕ} [inst : n.AtLeastTwo], Cardinal.aleph0 + OfNat.ofNat n = Cardinal.aleph0
-- Mathlib.NumberTheory.Dioph
/-- The set of places where two Diophantine functions are congruent modulo a third
is Diophantine.  -/
Dioph.modEq_dioph : ∀ {α : Type} {f g : (α → ℕ) → ℕ},
  Dioph.DiophFn f → Dioph.DiophFn g → ∀ {h : (α → ℕ) → ℕ}, Dioph.DiophFn h → Dioph {v | f v ≡ g v [MOD h v]}
-- Init.System.IOError
IO.Error.mkPermissionDeniedFile : String → UInt32 → String → IO.Error
-- Mathlib.Algebra.Module.LocalizedModule.IsLocalization
isLocalizedModule_iff_isLocalization : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Submonoid R} {A : Type u_2} {Aₛ : Type u_3} [inst_1 : CommSemiring A]
  [inst_2 : Algebra R A] [inst_3 : CommSemiring Aₛ] [inst_4 : Algebra A Aₛ] [inst_5 : Algebra R Aₛ]
  [inst_6 : IsScalarTower R A Aₛ],
  IsLocalizedModule S (IsScalarTower.toAlgHom R A Aₛ).toLinearMap ↔ IsLocalization (Algebra.algebraMapSubmonoid A S) Aₛ
-- Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
/-- **Chevalley's theorem** with complexity bound.

A constructible set of complexity at most `M` in `Spec R[X₁, ..., Xₘ]` gets mapped under
`f : R[Y₁, ..., Yₙ] → R[X₁, ..., Xₘ]` to a constructible set of complexity `O_{M, m, n}(1)` in
`Spec R[Y₁, ..., Yₙ]`.

See the module doc of `Mathlib/RingTheory/Spectrum/Prime/ChevalleyComplexity.lean` for an
explanation of this notion of complexity.  -/
chevalley_mvPolynomial_mvPolynomial : ∀ {R : Type u_2} [inst : CommRing R] {m n : ℕ} (f : MvPolynomial (Fin n) R →ₐ[R] MvPolynomial (Fin m) R) (k : ℕ)
  (d : Multiset (Fin m)) (S : PrimeSpectrum.ConstructibleSetData (MvPolynomial (Fin m) R)),
  (∀ C ∈ S, C.n ≤ k) →
    (∀ C ∈ S, ∀ (j : Fin C.n), (C.g j).degrees ≤ d) →
      (∀ (i : Fin n), (f (MvPolynomial.X i)).degrees ≤ d) →
        ∃ T,
          PrimeSpectrum.comap ↑f '' S.toSet = T.toSet ∧
            ∀ C ∈ T,
              C.n ≤ ChevalleyThm.numBound k m n d ∧
                ∀ (i : Fin C.n) (j : Fin n), MvPolynomial.degreeOf j (C.g i) ≤ ChevalleyThm.degBound k m n d
-- Lean.Data.FuzzyMatching
_private.Lean.Data.FuzzyMatching.0.Lean.FuzzyMatching.selectBest : Lean.FuzzyMatching.Score✝ → Lean.FuzzyMatching.Score✝ → Lean.FuzzyMatching.Score✝
-- Lean.Parser.Extension
Lean.Parser.addLeadingParser : Lean.Parser.ParserCategories →
  Lean.Name → Lean.Name → Lean.Parser.Parser → ℕ → Except String Lean.Parser.ParserCategories
-- Std.Data.HashSet.Basic
Std.HashSet.instInhabited : {α : Type u} → [inst : BEq α] → [inst_1 : Hashable α] → Inhabited (Std.HashSet α)
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.Hom.toHom : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {S : C} →
      {E : CategoryTheory.PreOneHypercover S} →
        {F : CategoryTheory.PreOneHypercover S} → E.Hom F → E.Hom F.toPreZeroHypercover
-- Mathlib.Topology.UniformSpace.AbstractCompletion
AbstractCompletion.map_coe : ∀ {α : Type uα} [inst : UniformSpace α] (pkg : AbstractCompletion.{vα, uα} α) {β : Type uβ} [inst_1 : UniformSpace β]
  (pkg' : AbstractCompletion.{vβ, uβ} β) {f : α → β},
  UniformContinuous f → ∀ (a : α), pkg.map pkg' f (pkg.coe a) = pkg'.coe (f a)
-- Mathlib.FieldTheory.Galois.IsGaloisGroup
/-- **Alias** of `IsGaloisGroup.map_quotientMk'`.

---

If `G` is a finite Galois group for `L/K`, `N` is a normal subgroup that is a Galois group for
`L/F`, and `H` is a subgroup that is a Galois group for `L/E` with `E ≤ F`, then the image of `H`
under the canonical quotient map `G → G ⧸ N` is a Galois group for `F/E`.  -/
IsGaloisGroup.quotientMap : ∀ (G : Type u_1) (K : Type u_3) (L : Type u_4) [inst : Group G] [inst_1 : Field K] [inst_2 : Field L]
  [inst_3 : Algebra K L] [inst_4 : MulSemiringAction G L] (H : Subgroup G) (F : IntermediateField K L) (N : Subgroup G)
  [inst_5 : N.Normal] [inst_6 : IsGaloisGroup (↥N) (↥F) L] (E : IntermediateField K L) [hE : IsGaloisGroup (↥H) (↥E) L]
  [Finite G] [IsGaloisGroup G K L] (h : E ≤ F), IsGaloisGroup ↥(Subgroup.map (QuotientGroup.mk' N) H) ↥E ↥F
-- Mathlib.Combinatorics.Enumerative.Stirling
_private.Mathlib.Combinatorics.Enumerative.Stirling.0.Nat.stirlingFirst.match_1.eq_4 : ∀ (motive : ℕ → ℕ → Sort u_1) (n k : ℕ) (h_1 : Unit → motive 0 0) (h_2 : (n : ℕ) → motive 0 n.succ)
  (h_3 : (n : ℕ) → motive n.succ 0) (h_4 : (n k : ℕ) → motive n.succ k.succ),
  (match n.succ, k.succ with
    | 0, 0 => h_1 ()
    | 0, n.succ => h_2 n
    | n.succ, 0 => h_3 n
    | n.succ, k.succ => h_4 n k) =
    h_4 n k
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.instNormedAlgebra : {A : Type u_1} →
  [inst : CStarAlgebra A] →
    [inst_1 : PartialOrder A] →
      [inst_2 : StarOrderedRing A] →
        {n : Type u_2} → [inst_3 : Fintype n] → [inst_4 : DecidableEq n] → NormedAlgebra ℂ (CStarMatrix n n A)
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.Clopens.coe_toCloseds : ∀ {α : Type u_2} [inst : TopologicalSpace α] (s : TopologicalSpace.Clopens α), ↑s.toCloseds = ↑s
-- Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
SSet.Subcomplex.preimage_ι : ∀ {X : SSet} (A : X.Subcomplex), A.preimage A.ι = ⊤
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.vadd_comp : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {R : Type u_3} {M : Type u_5}
  [inst_2 : TopologicalSpace M] [inst_3 : VAdd R M] [inst_4 : ContinuousConstVAdd R M] (r : R) (f : C(β, M))
  (g : C(α, β)), (r +ᵥ f).comp g = r +ᵥ f.comp g
-- Mathlib.Order.DirectedInverseSystem
/-- To define a function from the direct limit, it suffices to provide one function from each
component subject to a compatibility condition.  -/
DirectLimit.map : {ι : Type u_1} →
  [inst : Preorder ι] →
    {F₁ : ι → Type u_2} →
      {F₂ : ι → Type u_3} →
        {T₁ : ⦃i j : ι⦄ → i ≤ j → Sort u_6} →
          (f₁ : (i j : ι) → (h : i ≤ j) → T₁ h) →
            [inst_1 : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T₁ h) (F₁ i) (F₁ j)] →
              [inst_2 : DirectedSystem F₁ fun x1 x2 x3 => ⇑(f₁ x1 x2 x3)] →
                {T₂ : ⦃i j : ι⦄ → i ≤ j → Sort u_7} →
                  (f₂ : (i j : ι) → (h : i ≤ j) → T₂ h) →
                    [inst_3 : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T₂ h) (F₂ i) (F₂ j)] →
                      [inst_4 : DirectedSystem F₂ fun x1 x2 x3 => ⇑(f₂ x1 x2 x3)] →
                        [inst_5 : IsDirectedOrder ι] →
                          (ih : (i : ι) → F₁ i → F₂ i) →
                            (∀ (i j : ι) (h : i ≤ j) (x : F₁ i), (f₂ i j h) (ih i x) = ih j ((f₁ i j h) x)) →
                              DirectLimit F₁ f₁ → DirectLimit F₂ f₂
-- Lean.Compiler.IR.CompilerM
Lean.IR.logMessage : {α : Type} → [Std.ToFormat α] → α → Lean.IR.CompilerM Unit
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr
Std.Tactic.BVDecide.BVExpr.Cache.cast.congr_simp : ∀ {aig1 aig2 : Std.Sat.AIG Std.Tactic.BVDecide.BVBit} (cache cache_1 : Std.Tactic.BVDecide.BVExpr.Cache aig1),
  cache = cache_1 → ∀ (h : aig1.decls.size ≤ aig2.decls.size), cache.cast h = cache_1.cast h
-- Mathlib.Topology.Order.ScottTopology
Topology.WithScott.ofScott_symm_eq : ∀ {α : Type u_1}, Topology.WithScott.ofScott.symm = Topology.WithScott.toScott
-- Mathlib.Analysis.SpecialFunctions.Complex.Circle
Circle.isCoveringMap_exp : IsCoveringMap ⇑Circle.exp
-- Mathlib.Data.Num.Lemmas
Num.isOrderedCancelAddMonoid : IsOrderedCancelAddMonoid Num
-- Mathlib.Data.Nat.Choose.Lucas
/-- For primes `p`, `choose (p * a) (p * b)` is congruent to `choose a b` modulo `p`.
Also see `choose_mul_mul_modEq_choose` for the version with `ZMOD`.  -/
Choose.choose_mul_mul_modEq_choose_nat : ∀ {a b p : ℕ} [Fact (Nat.Prime p)], (p * a).choose (p * b) ≡ a.choose b [MOD p]
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
/-- `cfcₙHomSuperset` is continuous in the variable `a : A` when `s : Set 𝕜` is compact and `a`
varies over elements whose spectrum is contained in `s`, all of which satisfy the predicate `p`.  -/
continuous_cfcₙHomSuperset_left : ∀ {X : Type u_1} {𝕜 : Type u_2} {A : Type u_3} {p : A → Prop} [inst : RCLike 𝕜] [inst_1 : NonUnitalNormedRing A]
  [inst_2 : StarRing A] [inst_3 : NormedSpace 𝕜 A] [inst_4 : IsScalarTower 𝕜 A A] [inst_5 : SMulCommClass 𝕜 A A]
  [ContinuousStar A] [inst_7 : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p] [inst_8 : TopologicalSpace X]
  {s : Set 𝕜},
  IsCompact s →
    ∀ [hs0 : Fact (0 ∈ s)] (f : ContinuousMapZero (↑s) 𝕜) {a : X → A},
      Continuous a →
        ∀ (ha : ∀ (x : X), quasispectrum 𝕜 (a x) ⊆ s)
          (ha' : autoParam (∀ (x : X), p (a x)) continuous_cfcₙHomSuperset_left._auto_1),
          Continuous fun x => (cfcₙHomSuperset ⋯ ⋯) f
-- Init.System.ST
ST.Prim.Ref.swap : {σ α : Type} → ST.Ref σ α → α → ST σ α
-- Init.Data.List.Lemmas
List.getLast.eq_2 : ∀ {α : Type u} (a : α) (x_2 : [a] ≠ []), [a].getLast x_2 = a
-- Init.Data.List.Erase
List.eraseIdx_append_of_length_le : ∀ {α : Type u_1} {l : List α} {k : ℕ},
  l.length ≤ k → ∀ (l' : List α), (l ++ l').eraseIdx k = l ++ l'.eraseIdx (k - l.length)
-- Mathlib.CategoryTheory.Localization.Bifunctor
CategoryTheory.Localization.lift₂NatIso_hom : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_3} {D₂ : Type u_4} {E : Type u_5}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} D₁] [inst_3 : CategoryTheory.Category.{v_4, u_4} D₂]
  [inst_4 : CategoryTheory.Category.{v_5, u_5} E] (L₁ : CategoryTheory.Functor C₁ D₁)
  (L₂ : CategoryTheory.Functor C₂ D₂) (W₁ : CategoryTheory.MorphismProperty C₁)
  (W₂ : CategoryTheory.MorphismProperty C₂) [inst_5 : L₁.IsLocalization W₁] [inst_6 : L₂.IsLocalization W₂]
  [inst_7 : W₁.ContainsIdentities] [inst_8 : W₂.ContainsIdentities]
  (F₁ F₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ E))
  (F₁' F₂' : CategoryTheory.Functor D₁ (CategoryTheory.Functor D₂ E))
  [inst_9 : CategoryTheory.Localization.Lifting₂ L₁ L₂ W₁ W₂ F₁ F₁']
  [inst_10 : CategoryTheory.Localization.Lifting₂ L₁ L₂ W₁ W₂ F₂ F₂'] (e : F₁ ≅ F₂),
  (CategoryTheory.Localization.lift₂NatIso L₁ L₂ W₁ W₂ F₁ F₂ F₁' F₂' e).hom =
    CategoryTheory.Localization.lift₂NatTrans L₁ L₂ W₁ W₂ F₁ F₂ F₁' F₂' e.hom
-- Std.Data.HashMap.Basic
Std.HashMap.instSingletonProd : {α : Type u} → {β : Type v} → {x : BEq α} → {x_1 : Hashable α} → Singleton (α × β) (Std.HashMap α β)
-- Mathlib.Tactic.ReduceModChar
Tactic.ReduceModChar.CharP.isInt_of_mod : ∀ {e' r : ℤ} {α : Type u_1} [inst : Ring α] {n n' : ℕ},
  CharP α n →
    ∀ {e : α},
      Mathlib.Meta.NormNum.IsInt e e' →
        Mathlib.Meta.NormNum.IsNat n n' → Mathlib.Meta.NormNum.IsInt (e' % ↑n') r → Mathlib.Meta.NormNum.IsInt e r
-- Mathlib.CategoryTheory.Triangulated.Opposite.Functor
CategoryTheory.Functor.op_commShiftIso_hom_app : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.HasShift C ℤ]
  [inst_3 : CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [inst_4 : F.CommShift ℤ] (X : Cᵒᵖ) (n m : ℤ)
  (h : n + m = 0),
  (CategoryTheory.Functor.commShiftIso F.op n).hom.app X =
    CategoryTheory.CategoryStruct.comp
      (F.map ((CategoryTheory.Pretriangulated.shiftFunctorOpIso C n m h).hom.app X).unop).op
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.commShiftIso F m).inv.app (Opposite.unop X)).op
        ((CategoryTheory.Pretriangulated.shiftFunctorOpIso D n m h).inv.app (Opposite.op (F.obj (Opposite.unop X)))))
-- Std.Http.Protocol.H1
/-- The configuration.
 -/
Std.Http.Protocol.H1.Machine.config : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Machine dir → Std.Http.Protocol.H1.Config
-- Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basis
RootPairing.GeckConstruction.basis_A_eq : ∀ {ι : Type u_1} {K : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Fintype ι] [inst_1 : DecidableEq ι]
  [inst_2 : Field K] [inst_3 : CharZero K] [inst_4 : AddCommGroup M] [inst_5 : Module K M] [inst_6 : AddCommGroup N]
  [inst_7 : Module K N] {P : RootPairing ι K M N} [inst_8 : P.IsReduced] [inst_9 : P.IsCrystallographic]
  [inst_10 : P.IsIrreducible] [inst_11 : P.IsRootSystem] (b : P.Base),
  (RootPairing.GeckConstruction.basis b).A = b.cartanMatrix
-- Mathlib.Analysis.Complex.Circle
Circle.coe_pow : ∀ (z : Circle) (n : ℕ), ↑(z ^ n) = ↑z ^ n
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.support_eq : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : Zero β] (f : MeasureTheory.SimpleFunc α β),
  Function.support ⇑f = ⋃ y ∈ {y ∈ f.range | y ≠ 0}, ⇑f ⁻¹' {y}
-- Batteries.Lean.AttributeExtra
Lean.TagAttributeExtra.mk.injEq : ∀ (ext : Lean.PersistentEnvExtension Lean.Name Lean.Name Lean.NameSet) (base : Lean.NameHashSet)
  (ext_1 : Lean.PersistentEnvExtension Lean.Name Lean.Name Lean.NameSet) (base_1 : Lean.NameHashSet),
  ({ ext := ext, base := base } = { ext := ext_1, base := base_1 }) = (ext = ext_1 ∧ base = base_1)
-- Mathlib.Order.PartialSups
partialSups_bot : ∀ {α : Type u_1} {ι : Type u_3} [inst : SemilatticeSup α] [inst_1 : PartialOrder ι] [inst_2 : LocallyFiniteOrder ι]
  [inst_3 : OrderBot ι] (f : ι → α), (partialSups f) ⊥ = f ⊥
-- Mathlib.Topology.Separation.Basic
compl_singleton_mem_nhds_iff : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T1Space X] {x y : X}, {x}ᶜ ∈ nhds y ↔ y ≠ x
-- Lean.Parser.Term
Lean.Parser.Termination.decreasingBy.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Lean.Elab.Tactic.Omega.Core
Lean.Elab.Tactic.Omega.Justification.combo.injEq : ∀ {s t : Lean.Omega.Constraint} {x y : Lean.Omega.Coeffs} (a : ℤ) (j : Lean.Elab.Tactic.Omega.Justification s x) (b : ℤ)
  (k : Lean.Elab.Tactic.Omega.Justification t y) (j_1 : Lean.Elab.Tactic.Omega.Justification s x)
  (k_1 : Lean.Elab.Tactic.Omega.Justification t y),
  (Lean.Elab.Tactic.Omega.Justification.combo a j b k = Lean.Elab.Tactic.Omega.Justification.combo a j_1 b k_1) =
    (j = j_1 ∧ k = k_1)
-- Mathlib.Order.Filter.IndicatorFunction
Antitone.tendsto_indicator : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_5} [inst : Preorder ι] [inst_1 : Zero β] (s : ι → Set α),
  Antitone s →
    ∀ (f : α → β) (a : α), Filter.Tendsto (fun i => (s i).indicator f a) Filter.atTop (pure ((⋂ i, s i).indicator f a))
-- Mathlib.Data.Matrix.Basic
Subring.coe_matrix : ∀ {n : Type u_3} {R : Type u_14} [inst : NonAssocRing R] [inst_1 : Fintype n] [inst_2 : DecidableEq n] (S : Subring R),
  ↑S.matrix = S.toAddSubmonoid.matrix.carrier
-- Mathlib.Data.FunLike.IsApply
IsOneApplyEqSelf.one_apply_eq_self : ∀ {F : Type u_1} {α : outParam (Type u_2)} {inst : FunLike F α α} {inst_1 : One F} [self : IsOneApplyEqSelf F α]
  (x : α), 1 x = x
-- Mathlib.Algebra.Module.Presentation.Basic
Module.Presentation.toSolution : {A : Type u} →
  [inst : Ring A] →
    {M : Type v} →
      [inst_1 : AddCommGroup M] → [inst_2 : Module A M] → (self : Module.Presentation A M) → self.Solution M
-- Mathlib.RepresentationTheory.Rep.Basic
/-- The representation on `α →₀ k[G]` defined pointwise by the left regular representation on
`k[G]`.  -/
Rep.free : (k : Type u) → (G : Type v) → [inst : CommRing k] → [inst_1 : Monoid G] → Type u' → Rep.{max (max u u') v, u, v} k G
-- Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
Subgroup.commensurable_adjoinNegOne_self : ∀ {n : Type u_1} [inst : Fintype n] [inst_1 : DecidableEq n] {R : Type u_2} [inst_2 : Ring R] (𝒢 : Subgroup (GL n R)),
  𝒢.adjoinNegOne.Commensurable 𝒢
-- Mathlib.Order.PropInstances
Prop.decidablePredTop : {α : Type u} → DecidablePred ⊤
-- Mathlib.Order.Antisymmetrization
AntisymmRel.of_eq : ∀ {α : Type u_1} {r : α → α → Prop} [Std.Refl r] {a b : α}, a = b → AntisymmRel r a b
-- Mathlib.Order.RelSeries
RelSeries.tail_length : ∀ {α : Type u_1} {r : SetRel α α} (p : RelSeries r) (len_pos : p.length ≠ 0), (p.tail len_pos).length = p.length - 1
-- Mathlib.Algebra.Homology.Embedding.IsSupported
HomologicalComplex.instIsStrictlySupportedOppositeOpOp : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : HomologicalComplex C c') (e : c.Embedding c') [K.IsStrictlySupported e], K.op.IsStrictlySupported e.op
-- Mathlib.GroupTheory.Submonoid.Center
AddEquivClass.apply_mem_center_iff : ∀ {M : Type u_3} {N : Type u_1} {F : Type u_2} [inst : EquivLike F M N] [inst_1 : Add M] [inst_2 : Add N]
  [AddEquivClass F M N] (e : F) {x : M}, e x ∈ Set.addCenter N ↔ x ∈ Set.addCenter M