mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
CategoryTheory.Limits.WidePullbackShape.instDecidableEqHom : {J : Type u_1} → {a a_1 : CategoryTheory.Limits.WidePullbackShape J} → [DecidableEq J] → DecidableEq (a.Hom a_1)
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
MeasurableSpace.GenerateMeasurable.basic : ∀ {α : Type u_1} {s : Set (Set α)}, ∀ u ∈ s, MeasurableSpace.GenerateMeasurable s u
-- Mathlib.Algebra.BigOperators.Fin
Fin.prod_Ioo_castAdd : ∀ {M : Type u_2} [inst : CommMonoid M] {n : ℕ} (m : ℕ) (f : Fin (n + m) → M) (a b : Fin n),
  ∏ i ∈ Finset.Ioo (Fin.castAdd m a) (Fin.castAdd m b), f i = ∏ i ∈ Finset.Ioo a b, f (Fin.castAdd m i)
-- Mathlib.Algebra.Ring.Subring.MulOpposite
Subring.unop_sInf : ∀ {R : Type u_2} [inst : NonAssocRing R] (S : Set (Subring Rᵐᵒᵖ)), (sInf S).unop = sInf (Subring.op ⁻¹' S)
-- Aesop.RuleTac.Forward
Aesop.RuleTac.forwardConst : Lean.Name → Aesop.UnorderedArraySet Aesop.PremiseIndex → Bool → Aesop.RuleTac
-- Init.Data.Slice.List.Lemmas
List.toArray_mkSlice_roi_eq_toArray_mkSlice_roo : ∀ {α : Type u_1} {xs : List α} {lo : ℕ},
  Std.Slice.toArray (Std.Roi.Sliceable.mkSlice xs lo<...*) =
    Std.Slice.toArray (Std.Roo.Sliceable.mkSlice xs lo<...xs.length)
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.coe_constVSub_symm : ∀ (k : Type u_1) {P₁ : Type u_2} {V₁ : Type u_6} [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁]
  [inst_3 : AddTorsor V₁ P₁] (p : P₁), ⇑(AffineEquiv.constVSub k p).symm = fun v => -v +ᵥ p
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rcc.toList_toArray : ∀ {α : Type u} {r : Std.Rcc α} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [inst_4 : Std.Rxc.IsAlwaysFinite α], r.toArray.toList = r.toList
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Pretrivialization.restrictPreimage_baseSet : ∀ {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) {s : Set B} (hs : (s ∩ e.baseSet).Nonempty),
  (e.restrictPreimage hs).baseSet = Subtype.val ⁻¹' e.baseSet
-- Mathlib.CategoryTheory.Monoidal.FunctorCategory
/-- When `C` is any category, and `D` is a monoidal category,
the functor category `C ⥤ D` has a natural pointwise monoidal structure,
where `(F ⊗ G).obj X = F.obj X ⊗ G.obj X`.
 -/
CategoryTheory.Monoidal.functorCategoryMonoidal : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        [CategoryTheory.MonoidalCategory D] → CategoryTheory.MonoidalCategory (CategoryTheory.Functor C D)
-- Lean.Elab.InfoTree.Types
Lean.Elab.instInhabitedElabInfo.default : Lean.Elab.ElabInfo
-- Mathlib.Data.ENNReal.Basic
ENNReal.instNNRatCast : NNRatCast ENNReal
-- Mathlib.Combinatorics.Matroid.Sum
_private.Mathlib.Combinatorics.Matroid.Sum.0.Equiv.sumEquivSigmaBool.match_1.eq_2 : ∀ (α β : Type u_1) (motive : ((b : Bool) × bif b then β else α) → Sort u_2) (b : bif true then β else α)
  (h_1 : (a : bif false then β else α) → motive ⟨false, a⟩) (h_2 : (b : bif true then β else α) → motive ⟨true, b⟩),
  (match ⟨true, b⟩ with
    | ⟨false, a⟩ => h_1 a
    | ⟨true, b⟩ => h_2 b) =
    h_2 b
-- Mathlib.Algebra.Category.Grp.ZModuleEquivalence
/-- The forgetful functor from `ℤ` modules to `AddCommGrpCat` is essentially surjective.  -/
ModuleCat.forget₂_addCommGrp_essSurj : (CategoryTheory.forget₂ (ModuleCat ℤ) AddCommGrpCat).EssSurj
-- Init.Data.SInt.Basic
/-- Converts a natural number to a 64-bit signed integer, wrapping around to negative numbers on
overflow.

Examples:
 * `Nat.toInt64 127 = 127`
 * `Nat.toInt64 2_147_483_648 = 2_147_483_648`
 * `Nat.toInt64 9_223_372_036_854_775_807 = 9_223_372_036_854_775_807`
 * `Nat.toInt64 9_223_372_036_854_775_808 = -9_223_372_036_854_775_808`
 * `Nat.toInt64 18_446_744_073_709_551_618 = 0`
 -/
Nat.toInt64 : ℕ → Int64
-- Mathlib.Combinatorics.Matroid.Rank.Cardinal
/-- The rank (supremum of the cardinalities of bases) of a set `X` in a matroid `M`,
as a `Cardinal`. See `Matroid.eRk` for a better-behaved `ℕ∞`-valued version.  -/
Matroid.cRk : {α : Type u} → Matroid α → Set α → Cardinal.{u}
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.isIso_homologyMap_of_iso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) [CategoryTheory.IsIso φ] [inst_3 : S₁.HasHomology]
  [inst_4 : S₂.HasHomology], CategoryTheory.IsIso (CategoryTheory.ShortComplex.homologyMap φ)
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
/-- `p = 0` derived from the divisibility constraint `c` of the form `0 ∣ p`.  -/
Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.ofZeroDvd : Lean.Meta.Grind.Arith.Cutsat.DvdCnstr → Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof
-- Init.Data.Float.Model.Float
/-- Unpack a `Float.Model` into the corresponding `UnpackedFloat`.  -/
Float.Model.unpack : Float.Model → Float.Model.UnpackedFloat
-- Mathlib.GroupTheory.PushoutI
/-- All letters in the word are in the transversal.  -/
Monoid.PushoutI.NormalWord.normalized : ∀ {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [inst : (i : ι) → Group (G i)] [inst_1 : Group H]
  {φ : (i : ι) → H →* G i} {d : Monoid.PushoutI.NormalWord.Transversal φ} (self : Monoid.PushoutI.NormalWord d) (i : ι)
  (g : G i), ⟨i, g⟩ ∈ self.toList → g ∈ d.set i
-- Mathlib.Dynamics.Ergodic.Function
Ergodic.eq_const_of_compMeasurePreserving_eq : ∀ {α : Type u_1} {X : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace X]
  [TopologicalSpace.MetrizableSpace X] [Nonempty X] {f : α → α} (h : Ergodic f μ) {g : α →ₘ[μ] X},
  g.compMeasurePreserving f ⋯ = g → ∃ c, g = MeasureTheory.AEEqFun.const α c
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.minKey_eq_getElem_keysArray : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {he : t.isEmpty = false}, t.minKey he = t.keysArray[0]
-- Mathlib.Topology.Defs.Filter
/-- We say that `X` and `Y` are a locally compact pair of topological spaces,
if for any continuous map `f : X → Y`, a point `x : X`, and a neighbourhood `s ∈ 𝓝 (f x)`,
there exists a compact neighbourhood `K ∈ 𝓝 x` such that `f` maps `K` to `s`.

This is a technical assumption that appears in several theorems,
most notably in `ContinuousMap.continuous_comp'` and `ContinuousMap.continuous_eval`.
It is satisfied in two cases:

- if `X` is a locally compact topological space, for obvious reasons;
- if `X` is a weakly locally compact topological space and `Y` is an R₁ space;
  this fact is a simple generalization of the theorem
  saying that a weakly locally compact R₁ topological space is locally compact.
 -/
LocallyCompactPair : (X : Type u_3) → (Y : Type u_4) → [TopologicalSpace X] → [TopologicalSpace Y] → Prop
-- Mathlib.Algebra.Group.Opposite
MulOpposite.instSubNegMonoid : {α : Type u_1} → [SubNegMonoid α] → SubNegMonoid αᵐᵒᵖ
-- Mathlib.MeasureTheory.Function.SimpleFunc
/-- A `SimpleFunc` has finite measure support if it is equal to `0` outside of a set of finite
measure.  -/
MeasureTheory.SimpleFunc.FinMeasSupp : {α : Type u_1} →
  {β : Type u_2} → [Zero β] → {_m : MeasurableSpace α} → MeasureTheory.SimpleFunc α β → MeasureTheory.Measure α → Prop
-- Mathlib.CategoryTheory.Opposites
Quiver.Hom.unop_op' : ∀ {C : Type u₁} [inst : Quiver C] {X Y : Cᵒᵖ} {x : Opposite.unop Y ⟶ Opposite.unop X},
  Quiver.Hom.unop (Opposite.op x) = x
-- Mathlib.LinearAlgebra.BilinearForm.Orthogonal
LinearMap.BilinForm.orthogonal_orthogonal : ∀ {V : Type u_5} {K : Type u_6} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] [FiniteDimensional K V]
  {B : LinearMap.BilinForm K V}, B.Nondegenerate → B.IsRefl → ∀ (W : Submodule K V), B.orthogonal (B.orthogonal W) = W
-- Mathlib.Topology.Category.Profinite.Extend
/-- If the projection maps in the cone are epimorphic and the cone is limiting, then
`Profinite.Extend.functorOp` is final.
 -/
Profinite.Extend.functorOp_final : ∀ {I : Type u} [inst : CategoryTheory.SmallCategory I] [CategoryTheory.IsCofiltered I]
  {F : CategoryTheory.Functor I FintypeCat} (c : CategoryTheory.Limits.Cone (F.comp FintypeCat.toProfinite))
  (hc : CategoryTheory.Limits.IsLimit c) [∀ (i : I), CategoryTheory.Epi (c.π.app i)],
  (Profinite.Extend.functorOp c).Final
-- Mathlib.Algebra.Module.Presentation.Basic
Module.Relations.Solution.isPresentation_mk : ∀ {A : Type u} [inst : Ring A] {relations : Module.Relations A} {M : Type v} [inst_1 : AddCommGroup M]
  [inst_2 : Module A M] (solution : relations.Solution M),
  Submodule.span A (Set.range solution.var) = ⊤ →
    solution.π.ker = Submodule.span A (Set.range relations.relation) → solution.IsPresentation
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.ConnectedComponent.sound : ∀ {V : Type u} {G : SimpleGraph V} {v w : V}, G.Reachable v w → G.connectedComponentMk v = G.connectedComponentMk w
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineMap.homothety_neg_one_apply : ∀ {P₁ : Type u_2} {V₁ : Type u_6} [inst : AddCommGroup V₁] [inst_1 : AddTorsor V₁ P₁] {R' : Type u_10}
  [inst_2 : CommRing R'] [inst_3 : Module R' V₁] (c p : P₁),
  (AffineMap.homothety c (-1)) p = (AffineEquiv.pointReflection R' c) p
-- Mathlib.Algebra.Module.ZLattice.Summable
ZLattice.exists_finsetSum_norm_rpow_le_tsum : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E] (L : Submodule ℤ E)
  [DiscreteTopology ↥L],
  ∃ A > 0,
    ∀ r < -↑(Module.finrank ℤ ↥L),
      ∀ (s : Finset ↥L), ∑ z ∈ s, ‖z‖ ^ r ≤ A ^ r * ∑' (k : ℕ), ↑k ^ (↑(Module.finrank ℤ ↥L) - 1 + r)
-- Lean.Linter.Init
Lean.Linter.linter.all : Lean.Option Bool
-- Mathlib.Data.Complex.Basic
Complex.im_ofNat : ∀ (n : ℕ) [inst : n.AtLeastTwo], (OfNat.ofNat n).im = 0
-- Mathlib.SetTheory.Cardinal.Cofinality.Basic
/-- The cofinality of a preorder is the smallest cardinality of a cofinal subset.  -/
Order.cof : (α : Type u) → [Preorder α] → Cardinal.{u}
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
/-- Like `mapDomain_add`, but for the skewed convolutive multiplication we define in this
file. This theorem holds assuming that `(hf : ∀ (a : α) (x : β), a • x = (f a) • x)`.  -/
SkewMonoidAlgebra.mapDomain_mul : ∀ {α : Type u_3} {α₂ : Type u_4} {β : Type u_5} {F : Type u_6} [inst : Semiring β] [inst_1 : Monoid α]
  [inst_2 : Monoid α₂] [inst_3 : FunLike F α α₂] [inst_4 : MulSemiringAction α β] [inst_5 : MulSemiringAction α₂ β]
  [MulHomClass F α α₂] {f : F} (x y : SkewMonoidAlgebra β α),
  (∀ (a : α) (x : β), a • x = f a • x) →
    (SkewMonoidAlgebra.mapDomain ⇑f) (x * y) = (SkewMonoidAlgebra.mapDomain ⇑f) x * (SkewMonoidAlgebra.mapDomain ⇑f) y
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instNatCast : {α : Type u_1} → {l : Filter α} → {M : Type u_5} → [NatCast M] → NatCast (l.Germ M)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getD_eq_fallback_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {a : α}
  {fallback : β a}, m.contains a = false → m.getD a fallback = fallback
-- Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
/-- The equivalence `ToType (∏ᶜ F) ≃ ∀ j, ToType (F j)` if `F : J → C` is a family of objects
in a concrete category `C`.  -/
CategoryTheory.Limits.Concrete.productEquiv : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {FC : C → C → Type u_1} →
      {CC : C → Type (max w v)} →
        [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] →
          [inst_2 : CategoryTheory.ConcreteCategory C FC] →
            {J : Type w} →
              (F : J → C) →
                [inst_3 : CategoryTheory.Limits.HasProduct F] →
                  [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Discrete.functor F) (CategoryTheory.forget C)] →
                    CategoryTheory.ToType (∏ᶜ F) ≃ ((j : J) → CategoryTheory.ToType (F j))
-- Mathlib.Dynamics.TopologicalEntropy.NetEntropy
/-- The largest cardinality of a `(U, n)`-dynamical net of `F`. Takes values in `ℕ∞`, and is
infinite if and only if `F` admits nets of arbitrarily large size.  -/
Dynamics.netMaxcard : {X : Type u_1} → (X → X) → Set X → SetRel X X → ℕ → ℕ∞
-- Mathlib.Topology.CWComplex.Abstract.Basic
/-- For each `n : ℕ`, this is the family of morphisms which sends the unique
element of `Unit` to `diskBoundaryInclusion n : ∂𝔻 n ⟶ 𝔻 n`.  -/
TopCat.RelativeCWComplex.basicCell : (n : ℕ) → Unit → (TopCat.diskBoundary n ⟶ TopCat.disk n)
-- Mathlib.FieldTheory.Galois.Basic
/-- The Galois correspondence as a `GaloisCoinsertion`.  -/
IsGalois.galoisCoinsertionIntermediateFieldSubgroup : {F : Type u_1} →
  [inst : Field F] →
    {E : Type u_2} →
      [inst_1 : Field E] →
        [inst_2 : Algebra F E] →
          [FiniteDimensional F E] →
            [IsGalois F E] →
              GaloisCoinsertion (⇑OrderDual.toDual ∘ IntermediateField.fixingSubgroup)
                (IntermediateField.fixedField ∘ ⇑OrderDual.toDual)
-- Lean.Data.JsonRpc
/-- The JSON sent is not a valid Request object.  -/
Lean.JsonRpc.ErrorCode.invalidRequest : Lean.JsonRpc.ErrorCode
-- Mathlib.Order.Interval.Set.Pi
Set.image_mulSingle_Ico_right : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : DecidableEq ι] [inst_1 : (i : ι) → PartialOrder (α i)]
  [inst_2 : (i : ι) → One (α i)] (i : ι) (b : α i), Pi.mulSingle i '' Set.Ico 1 b = Set.Ico 1 (Pi.mulSingle i b)
-- Mathlib.Logic.Equiv.Defs
Equiv.ext : ∀ {α : Sort u} {β : Sort v} {f g : α ≃ β}, (∀ (x : α), f x = g x) → f = g
-- Mathlib.Data.Set.Insert
Set.exists_mem_insert : ∀ {α : Type u_1} {P : α → Prop} {a : α} {s : Set α}, (∃ x ∈ insert a s, P x) ↔ P a ∨ ∃ x ∈ s, P x
-- Mathlib.Algebra.AddConstMap.Equiv
/-- Group equivalence between `G ≃+c[a, a] G` and the units of `G →+c[a, a] G`.  -/
AddConstEquiv.equivUnits : {G : Type u_1} → [inst : Add G] → {a : G} → AddConstEquiv G G a a ≃* (AddConstMap G G a a)ˣ
-- Mathlib.Logic.Equiv.Basic
/-- The type of integer numbers is equivalent to `ℕ ⊕ ℕ`.  -/
Equiv.intEquivNatSumNat : ℤ ≃ ℕ ⊕ ℕ
-- Mathlib.RingTheory.OrderOfVanishing.Basic
Ring.ordMonoidWithZeroHom_eq_coe : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : Nontrivial R] {x : R},
  x ∈ nonZeroDivisors R → ∀ {n : ℕ}, Ring.ord R x = ↑n → (Ring.ordMonoidWithZeroHom R) x = ↑(Multiplicative.ofAdd ↑n)
-- Mathlib.Topology.Algebra.Module.Alternating.Topology
ContinuousAlternatingMap.isUniformEmbedding_toContinuousMultilinearMap : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_4} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : Module 𝕜 E] [inst_3 : TopologicalSpace E] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : UniformSpace F] [inst_7 : IsUniformAddGroup F],
  IsUniformEmbedding ContinuousAlternatingMap.toContinuousMultilinearMap
-- Mathlib.RingTheory.Teichmuller
Perfection.teichmullerFun_spec' : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {R : Type u_1} [inst_1 : CommRing R] {I : Ideal R} [inst_2 : CharP (R ⧸ I) p]
  [inst_3 : IsAdicComplete I R] {x : Perfection (R ⧸ I) p} {y : R},
  (∃ N, ∀ n ≥ N, ∃ z, (Ideal.Quotient.mk I) z = (Perfection.coeff (R ⧸ I) p n) x ∧ z ^ p ^ n ≡ y [SMOD I ^ (n + 1)]) →
    x.teichmullerFun = y
-- Lean.Elab.Tactic.Omega.Core
/-- Representation of the data required to run Fourier-Motzkin elimination on a variable.  -/
Lean.Elab.Tactic.Omega.Problem.FourierMotzkinData : Type
-- Mathlib.LinearAlgebra.Matrix.RowCol
Matrix.replicateRow_injective : ∀ {n : Type u_3} {α : Type v} {ι : Type u_6} [Nonempty ι], Function.Injective (Matrix.replicateRow ι)
-- Mathlib.Data.PFunctor.Multivariate.W
MvPFunctor.mvfunctorW : {n : ℕ} → (P : MvPFunctor.{u} (n + 1)) → MvFunctor P.W
-- Mathlib.RingTheory.Ideal.Operations
IsCoprime.codisjoint : ∀ {R : Type u} [inst : CommSemiring R] {I J : Ideal R}, IsCoprime I J → Codisjoint I J
-- Mathlib.Analysis.Calculus.ContDiff.Basic
/-- The iterated derivative within a set of the composition with a linear map on the right is
obtained by composing the iterated derivative with the linear map.  -/
ContinuousLinearMap.iteratedFDerivWithin_comp_right : ∀ {𝕜 : 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] {s : Set E} {n : WithTop ℕ∞} {f : E → F} (g : G →L[𝕜] E),
  ContDiffOn 𝕜 n f s →
    UniqueDiffOn 𝕜 s →
      UniqueDiffOn 𝕜 (⇑g ⁻¹' s) →
        ∀ {x : G},
          g x ∈ s →
            ∀ {i : ℕ},
              ↑i ≤ n →
                iteratedFDerivWithin 𝕜 i (f ∘ ⇑g) (⇑g ⁻¹' s) x =
                  (iteratedFDerivWithin 𝕜 i f s (g x)).compContinuousLinearMap fun x => g
-- Mathlib.Data.Nat.MaxPowDiv
Nat.maxPowDvdDiv_one_left : ∀ (n : ℕ), Nat.maxPowDvdDiv 1 n = (0, n)
-- Init.Data.Slice.Array.Basic
instSliceableArrayNatSubarray_1 : {α : Type u} → Std.Rco.Sliceable (Array α) ℕ (Subarray α)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.get_insert_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k : α} {v : β k}, (t.insert k v).get k ⋯ = v
-- Init.Data.Nat.Bitwise.Lemmas
Nat.testBit_succ : ∀ (x i : ℕ), x.testBit i.succ = (x / 2).testBit i
-- Mathlib.Analysis.Fourier.AddCircle
fourierCoeff_fourier : ∀ {T : ℝ} [hT : Fact (0 < T)] (n : ℤ), fourierCoeff ⇑(fourier n) = Pi.single n 1
-- Mathlib.Algebra.Homology.EulerCharacteristic
/-- Signs alternate in the backward direction of the complex shape.  -/
ComplexShape.χ_prev : ∀ {ι : Type u_1} (c : ComplexShape ι) [inst : c.EulerCharSigns] {i j : ι}, c.Rel i j → c.χ i = -c.χ j
-- Mathlib.Tactic.Simps.Basic
/-- `@[simps (attr := attr1, attr2, ...)]` adds additional attributes to all lemmas
generated by `simps`.  -/
Lean.Parser.Attr.simpsConfigAttrItem : Lean.ParserDescr
-- Mathlib.LinearAlgebra.Finsupp.Supported
Finsupp.codisjoint_supported_supported_iff : ∀ {α : Type u_1} {M : Type u_2} {R : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [Nontrivial M] {s t : Set α}, Codisjoint (Finsupp.supported M R s) (Finsupp.supported M R t) ↔ Codisjoint s t
-- Mathlib.LinearAlgebra.Matrix.DotProduct
dotProduct_nonneg_of_nonneg : ∀ {n : Type u_2} {R : Type u_4} [inst : Semiring R] [inst_1 : PartialOrder R] [IsOrderedRing R] [inst_3 : Fintype n]
  {v w : n → R}, 0 ≤ v → 0 ≤ w → 0 ≤ v ⬝ᵥ w
-- Mathlib.Data.Finset.Card
/-- Given a bijection from a finite set `s` to a finite set `t`, the cardinalities of `s` and `t`
are equal.

The difference with `Finset.card_bij'` is that the bijection is specified as a surjective injection,
rather than by an inverse function.

The difference with `Finset.card_nbij` is that the bijection is allowed to use membership of the
domain, rather than being a non-dependent function.  -/
Finset.card_bij : ∀ {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} (i : (a : α) → a ∈ s → β),
  (∀ (a : α) (ha : a ∈ s), i a ha ∈ t) →
    (∀ (a₁ : α) (ha₁ : a₁ ∈ s) (a₂ : α) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂) →
      (∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), i a ha = b) → s.card = t.card
-- Lean.Compiler.CSimpAttr
Lean.Compiler.CSimp.Entry.fromDeclName : Lean.Compiler.CSimp.Entry → Lean.Name
-- Mathlib.Data.Ordmap.Ordset
Ordnode.Bounded.eq_def : ∀ {α : Type u_1} [inst : Preorder α] (x : Ordnode α) (x_1 : WithBot α) (x_2 : WithTop α),
  x.Bounded x_1 x_2 =
    match x, x_1, x_2 with
    | Ordnode.nil, some a, some b => a < b
    | Ordnode.nil, x, x_3 => True
    | Ordnode.node size l x r, o₁, o₂ => l.Bounded o₁ ↑x ∧ r.Bounded (↑x) o₂
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.nonempty_neg : ∀ {α : Type u_2} [inst : InvolutiveNeg α] {s : Set α}, (-s).Nonempty ↔ s.Nonempty
-- Std.Async.System
Std.Async.System.CPUTimes.mk.injEq : ∀
  (userTime niceTime systemTime idleTime interruptTime userTime_1 niceTime_1 systemTime_1 idleTime_1 interruptTime_1 :
    Std.Time.Millisecond.Offset),
  ({ userTime := userTime, niceTime := niceTime, systemTime := systemTime, idleTime := idleTime,
        interruptTime := interruptTime } =
      { userTime := userTime_1, niceTime := niceTime_1, systemTime := systemTime_1, idleTime := idleTime_1,
        interruptTime := interruptTime_1 }) =
    (userTime = userTime_1 ∧
      niceTime = niceTime_1 ∧ systemTime = systemTime_1 ∧ idleTime = idleTime_1 ∧ interruptTime = interruptTime_1)
-- Mathlib.Algebra.Module.Submodule.Ker
LinearMap.ker_neg : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_7} [inst : Ring R] [inst_1 : Ring R₂]
  [inst_2 : AddCommGroup M] [inst_3 : AddCommGroup M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  (f : M →ₛₗ[τ₁₂] M₂), (-f).ker = f.ker
-- Mathlib.GroupTheory.Complement
Subgroup.isComplement'_top_left : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G}, ⊤.IsComplement' H ↔ H = ⊥
-- Mathlib.CategoryTheory.Sites.Point.Basic
CategoryTheory.GrothendieckTopology.Point.presheafFiberCompIso.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point)
  {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A] {B : Type u''}
  [inst_2 : CategoryTheory.Category.{v'', u''} B] [inst_3 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A]
  [inst_4 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v'', u''} B] (F : CategoryTheory.Functor A B)
  [inst_5 : CategoryTheory.LocallySmall.{w, v, u} C]
  [inst_6 : CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', v'', u', u''} F],
  Φ.presheafFiberCompIso F = Φ.presheafFiberCompIso F
-- Mathlib.Algebra.Field.Defs
/-- Scalar multiplication by a nonnegative rational number.

Unless there is a risk of a `Module ℚ≥0 _` instance diamond, write `nnqsmul := _`. This will set
`nnqsmul` to `(NNRat.cast · * ·)` thanks to unification in the default proof of `nnqsmul_def`.

Do not use directly. Instead use the `•` notation.  -/
Field.nnqsmul : {K : Type u} → [self : Field K] → ℚ≥0 → K → K
-- Mathlib.CategoryTheory.Products.Basic
CategoryTheory.Functor.prod_map : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} D] (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C D)
  {X Y : A × C} (f : X ⟶ Y), (F.prod G).map f = CategoryTheory.Prod.mkHom (F.map f.1) (G.map f.2)
-- Mathlib.Order.Comparable
instTransAntisymmRelLeIncompRel : {α : Type u_1} →
  [inst : Preorder α] →
    Trans (AntisymmRel fun x1 x2 => x1 ≤ x2) (IncompRel fun x1 x2 => x1 ≤ x2) (IncompRel fun x1 x2 => x1 ≤ x2)
-- Mathlib.Data.PEquiv
Equiv.toPEquiv_symm : ∀ {α : Type u_1} {β : Type u_2} (f : α ≃ β), f.symm.toPEquiv = f.toPEquiv.symm
-- Mathlib.Order.Interval.Finset.Fin
Fin.Icc_add_one_eq_Ioc : ∀ {n : ℕ} {a b : Fin n}, ↑a + 1 < n → Finset.Icc (a + 1) b = Finset.Ioc a b
-- Mathlib.Analysis.Meromorphic.Basic
Meromorphic.prod : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {ι : Type u_5} {s : Finset ι} {F : ι → 𝕜 → 𝕜'},
  (∀ σ ∈ s, Meromorphic (F σ)) → Meromorphic (∏ n ∈ s, F n)
-- Mathlib.Algebra.Polynomial.Laurent
/-- Suppose that `Q` is a statement about Laurent polynomials such that
* `Q` is true on *ordinary* polynomials;
* `Q (f * T)` implies `Q f`;

it follow that `Q` is true on all Laurent polynomials.  -/
LaurentPolynomial.reduce_to_polynomial_of_mul_T : ∀ {R : Type u_1} [inst : Semiring R] (f : LaurentPolynomial R) {Q : LaurentPolynomial R → Prop},
  (∀ (f : Polynomial R), Q (Polynomial.toLaurent f)) →
    (∀ (f : LaurentPolynomial R), Q (f * LaurentPolynomial.T 1) → Q f) → Q f
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.Poly.denote_sort : ∀ (ctx : Nat.Internal.Linear.Context) (m : Nat.Internal.Linear.Poly),
  Nat.Internal.Linear.Poly.denote ctx m.norm = Nat.Internal.Linear.Poly.denote ctx m
-- Init.Data.Option.Lemmas
Option.pmap_none' : ∀ {α : Type u_1} {β : Type u_2} {x : Option α} {p : α → Prop} {f : (a : α) → p a → β},
  x = none → ∀ {h : ∀ (a : α), x = some a → p a}, Option.pmap f x h = none
-- Mathlib.CategoryTheory.Category.Pointed
/-- the distinguished element  -/
Pointed.point : (self : Pointed) → self.X