mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Elab.PreDefinition.WF.GuessLex
Lean.Elab.WF.GuessLex.SavedLocalContext.mk.inj : ∀ {savedLocalContext : Lean.LocalContext} {savedLocalInstances : Lean.LocalInstances}
  {savedState : Lean.Meta.SavedState} {savedLocalContext_1 : Lean.LocalContext}
  {savedLocalInstances_1 : Lean.LocalInstances} {savedState_1 : Lean.Meta.SavedState},
  { savedLocalContext := savedLocalContext, savedLocalInstances := savedLocalInstances, savedState := savedState } =
      { savedLocalContext := savedLocalContext_1, savedLocalInstances := savedLocalInstances_1,
        savedState := savedState_1 } →
    savedLocalContext = savedLocalContext_1 ∧ savedLocalInstances = savedLocalInstances_1 ∧ savedState = savedState_1
-- Std.Http.Data.Status
/-- 200 OK
 -/
Std.Http.Status.ok : Std.Http.Status
-- Init.Data.UInt.Lemmas
UInt64.add_neg_eq_sub : ∀ {a b : UInt64}, a + -b = a - b
-- Mathlib.GroupTheory.Complement
AddSubgroup.IsComplement.toRightFun_add_neg_mem : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G} {T : Set G} (hT : AddSubgroup.IsComplement (↑H) T) (g : G),
  ↑(hT.toRightFun g) + -g ∈ H
-- Init.Data.String.Pattern.Basic
String.Slice.Pattern.ToBackwardSearcher.DefaultBackwardSearcher.instIteratorIdSearchStepOfBackwardPattern : {ρ : Type} →
  (pat : ρ) →
    (s : String.Slice) →
      [String.Slice.Pattern.BackwardPattern pat] →
        Std.Iterator (String.Slice.Pattern.ToBackwardSearcher.DefaultBackwardSearcher pat s) Id
          (String.Slice.Pattern.SearchStep s)
-- Mathlib.Topology.UniformSpace.Dini
/-- **Dini's theorem**: if `F n` is a monotone decreasing collection of continuous functions on a
set `s` converging pointwise to a continuous function `f`, then `F n` converges locally uniformly
to `f`.  -/
Antitone.tendstoLocallyUniformlyOn_of_forall_tendsto : ∀ {ι : Type u_1} {α : Type u_2} {G : Type u_3} [inst : Preorder ι] [inst_1 : TopologicalSpace α]
  [inst_2 : NormedAddCommGroup G] [inst_3 : Lattice G] [HasSolidNorm G] [IsOrderedAddMonoid G] {F : ι → α → G}
  {f : α → G} {s : Set α},
  (∀ (i : ι), ContinuousOn (F i) s) →
    (∀ x ∈ s, Antitone fun x_1 => F x_1 x) →
      ContinuousOn f s →
        (∀ x ∈ s, Filter.Tendsto (fun x_1 => F x_1 x) Filter.atTop (nhds (f x))) →
          TendstoLocallyUniformlyOn F f Filter.atTop s
-- Mathlib.CategoryTheory.Limits.Types.Coproducts
/-- The bijection from the sigma type to the point of a colimit cofan
of a functor to types.  -/
CategoryTheory.Limits.CofanTypes.equivOfIsColimit : {C : Type u} →
  {F : C → Type v} →
    {c : CategoryTheory.Limits.CofanTypes F} → CategoryTheory.Functor.CoconeTypes.IsColimit c → (i : C) × F i ≃ c.pt
-- Mathlib.SetTheory.Ordinal.CantorNormalForm
/-- The Cantor normal form of an ordinal `o` is the list of coefficients and exponents in the
base-`b` expansion of `o`.

We special-case `CNF 0 o = CNF 1 o = [(0, o)]` for `o ≠ 0`.

`CNF b (b ^ u₁ * v₁ + b ^ u₂ * v₂) = [(u₁, v₁), (u₂, v₂)]`  -/
Ordinal.CNF : Ordinal.{u_1} → Ordinal.{u_1} → List (Ordinal.{u_1} × Ordinal.{u_1})
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
EisensteinSeries.tsum_tsum_symmetricIco_sub_eq : ∀ (z : UpperHalfPlane),
  ∑' (m : ℤ), ∑'[SummationFilter.symmetricIco ℤ] (n : ℤ), (1 / (↑m * ↑z + ↑n) - 1 / (↑m * ↑z + ↑n + 1)) = 0
-- Mathlib.CategoryTheory.Abelian.Opposite
CategoryTheory.kernel.ι_unop : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C] {A B : Cᵒᵖ}
  (g : A ⟶ B),
  (CategoryTheory.Limits.kernel.ι g.unop).op =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π g) (CategoryTheory.kernelUnopOp g).inv)
-- Mathlib.Analysis.Seminorm
Seminorm.continuous : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : NontriviallyNormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousConstSMul 𝕜 E] {p : Seminorm 𝕜 E} {r : ℝ},
  p.ball 0 r ∈ nhds 0 → Continuous ⇑p
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.isEmpty_iff_forall_contains : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → (t.isEmpty = true ↔ ∀ (a : α), Std.DTreeMap.Internal.Impl.contains a t = false)
-- Mathlib.RingTheory.DedekindDomain.SelmerGroup
/-- The multiplicative `v`-adic valuation on `Kˣ`.  -/
IsDedekindDomain.HeightOneSpectrum.valuationOfNeZero : {R : Type u} →
  [inst : CommRing R] →
    [IsDedekindDomain R] →
      {K : Type v} →
        [inst_2 : Field K] →
          [inst_3 : Algebra R K] → [IsFractionRing R K] → IsDedekindDomain.HeightOneSpectrum R → Kˣ →* Multiplicative ℤ
-- Batteries.Data.BinomialHeap.Basic
/-- `O(n)`. Convert the heap to an array in arbitrary order.  -/
Batteries.BinomialHeap.Imp.Heap.toArrayUnordered : {α : Type u_1} → Batteries.BinomialHeap.Imp.Heap α → Array α
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.Ordered.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (t : Std.DTreeMap.Internal.Impl α β),
  t.Ordered = List.Pairwise (fun a b => compare a.fst b.fst = Ordering.lt) t.toListModel
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.equalizerComparison_comp_π : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] (f g : X ⟶ Y) {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D)
  [inst_2 : CategoryTheory.Limits.HasEqualizer f g] [inst_3 : CategoryTheory.Limits.HasEqualizer (G.map f) (G.map g)],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.equalizerComparison f g G)
      (CategoryTheory.Limits.equalizer.ι (G.map f) (G.map g)) =
    G.map (CategoryTheory.Limits.equalizer.ι f g)
-- Init.Internal.Order.Lemmas
Lean.Order.List.monotone_mapM : ∀ {m : Type u → Type v} [inst : Monad m] [inst_1 : (α : Type u) → Lean.Order.PartialOrder (m α)] [Lean.Order.MonoBind m]
  {α β : Type u} {γ : Type w} [inst_3 : Lean.Order.PartialOrder γ] (f : γ → α → m β) (xs : List α),
  Lean.Order.monotone f → Lean.Order.monotone fun x => List.mapM (f x) xs
-- Mathlib.Algebra.Group.Hom.Defs
AddMonoidHom.comp_zero : ∀ {M : Type u_4} {N : Type u_5} {P : Type u_6} [inst : AddZero M] [inst_1 : AddZeroClass N] [inst_2 : AddZeroClass P]
  (f : N →+ P), f.comp 0 = 0
-- Mathlib.AlgebraicGeometry.Stalk
AlgebraicGeometry.Scheme.instIsOverMapStalkMapOverInferInstanceOverClass : ∀ {X Y : AlgebraicGeometry.Scheme} [inst : X.Over Y] {x : ↥X},
  AlgebraicGeometry.Scheme.Hom.IsOver (AlgebraicGeometry.Spec.map (AlgebraicGeometry.Scheme.Hom.stalkMap (X ↘ Y) x)) Y
-- Std.Tactic.BVDecide.Normalize.BitVec
Std.Tactic.BVDecide.Normalize.BitVec.add_neg_mul'' : ∀ {w : ℕ} {x y : BitVec w}, ~~~(x * y + x) + 1#w = x * ~~~y
-- Mathlib.Geometry.RingedSpace.Basic
AlgebraicGeometry.RingedSpace.basicOpen_res : ∀ (X : AlgebraicGeometry.RingedSpace) {U V : (TopologicalSpace.Opens ↑↑X.toPresheafedSpace)ᵒᵖ} (i : U ⟶ V)
  (f : ↑(X.presheaf.obj U)),
  X.basicOpen ((CategoryTheory.ConcreteCategory.hom (X.presheaf.map i)) f) = Opposite.unop V ⊓ X.basicOpen f
-- Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Fin.accumulate_apply : ∀ (n m : ℕ) (t : Fin n → ℕ) (j : Fin m), (Fin.accumulate n m) t j = ∑ i with ↑j ≤ ↑i, t i
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.mk_coeFn : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace β]
  (f : α →ₘ[μ] β), MeasureTheory.AEEqFun.mk ↑f ⋯ = f
-- Mathlib.Analysis.Calculus.DifferentialForm.Basic
extDeriv_add : ∀ {𝕜 : 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] {n : ℕ}
  {ω₁ ω₂ : E → E [⋀^Fin n]→L[𝕜] F} {x : E},
  DifferentiableAt 𝕜 ω₁ x → DifferentiableAt 𝕜 ω₂ x → extDeriv (ω₁ + ω₂) x = extDeriv ω₁ x + extDeriv ω₂ x
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.minEntry!_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited (α × β)], t₁.Equiv t₂ → t₁.minEntry! = t₂.minEntry!
-- Lean.Data.Json.Basic
_private.Lean.Data.Json.Basic.0.Lean.JsonNumber.countDigits.loop : ℕ → ℕ → ℕ
-- Lean.Util.Trace
/-- `MonadExcept` variant that is expected to catch all exceptions of the given type in case the
standard instance doesn't.

In most circumstances, we want to let runtime exceptions during term elaboration bubble up to the
command elaborator (see `Core.tryCatch`). However, in a few cases like building the trace tree, we
really need to handle (and then re-throw) every exception lest we end up with a broken tree.
 -/
Lean.MonadAlwaysExcept : outParam (Type u) → (Type u → Type v) → Type (max (u + 1) v)
-- Mathlib.CategoryTheory.EffectiveEpi.Basic
CategoryTheory.EffectiveEpi.desc.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y W : C} (f f_1 : Y ⟶ X) (e_f : f = f_1)
  [inst_1 : CategoryTheory.EffectiveEpi f] (e e_1 : Y ⟶ W) (e_e : e = e_1)
  (h :
    ∀ {Z : C} (g₁ g₂ : Z ⟶ Y),
      CategoryTheory.CategoryStruct.comp g₁ f = CategoryTheory.CategoryStruct.comp g₂ f →
        CategoryTheory.CategoryStruct.comp g₁ e = CategoryTheory.CategoryStruct.comp g₂ e),
  CategoryTheory.EffectiveEpi.desc f e h = CategoryTheory.EffectiveEpi.desc f_1 e_1 ⋯
-- Std.Tactic.Do.Syntax
Lean.Parser.Tactic.mrevertPat_ : Lean.ParserDescr
-- Mathlib.Order.Filter.Basic
Filter.instTransSetMem : {α : Type u} → Trans (fun x1 x2 => x1 ⊇ x2) (fun x1 x2 => x1 ∈ x2) fun x1 x2 => x1 ∈ x2
-- Mathlib.AlgebraicGeometry.Morphisms.Proper
AlgebraicGeometry.isProper_iff : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y),
  AlgebraicGeometry.IsProper f ↔
    AlgebraicGeometry.IsSeparated f ∧ AlgebraicGeometry.UniversallyClosed f ∧ AlgebraicGeometry.LocallyOfFiniteType f
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.get!_eq_getElem! : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [inst : Inhabited β] {a : α},
  t.get! a = t[a]!
-- Init.Data.Fin.Lemmas
Fin.cast_natAdd_left : ∀ {n m m' : ℕ} (i : Fin n) (h : m' + n = m + n), Fin.cast h (Fin.natAdd m' i) = Fin.natAdd m i
-- Init.Data.Repr
instReprDecidable : {p : Prop} → Repr (Decidable p)
-- Init.Prelude
/-- `LE α` is the typeclass which supports the notation `x ≤ y` where `x y : α`. -/
LE : Type u → Type u
-- Mathlib.LinearAlgebra.AffineSpace.Combination
/-- A point in the `affineSpan` of an indexed family is an
`affineCombination` with sum of weights 1. See also
`eq_affineCombination_of_mem_affineSpan_of_fintype`.  -/
eq_affineCombination_of_mem_affineSpan : ∀ {ι : Type u_1} {k : Type u_2} {V : Type u_3} {P : Type u_4} [inst : Ring k] [inst_1 : AddCommGroup V]
  [inst_2 : Module k V] [inst_3 : AddTorsor V P] {p1 : P} {p : ι → P},
  p1 ∈ affineSpan k (Set.range p) → ∃ s w, ∑ i ∈ s, w i = 1 ∧ p1 = (Finset.affineCombination k s p) w
-- Mathlib.CategoryTheory.Sites.LocallyInjective
CategoryTheory.Presheaf.equalizerSieve_eq_top_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {FD : D → D → Type u_1} {CD : D → Type w} [inst_2 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)]
  [inst_3 : CategoryTheory.ConcreteCategory D FD] {F : CategoryTheory.Functor Cᵒᵖ D} {X : Cᵒᵖ}
  (x y : CategoryTheory.ToType (F.obj X)), CategoryTheory.Presheaf.equalizerSieve x y = ⊤ ↔ x = y
-- Lean.Parser.Term
Lean.Parser.Term.letIdLhs.formatter : Lean.PrettyPrinter.Formatter
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Fin
Fin.reduceAnd : Lean.Meta.Simp.DSimproc
-- Init.Data.Range.Polymorphic.PRange
Std.Rco.mk.injEq : ∀ {α : Type u} (lower upper lower_1 upper_1 : α),
  ((lower...upper) = lower_1...upper_1) = (lower = lower_1 ∧ upper = upper_1)
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.LeftFraction.Localization.Qiso_hom_inv_id_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W : CategoryTheory.MorphismProperty C}
  [inst_1 : W.HasLeftCalculusOfFractions] {X Y : C} (s : X ⟶ Y) (hs : W s)
  {Z : CategoryTheory.MorphismProperty.LeftFraction.Localization W}
  (h : (CategoryTheory.MorphismProperty.LeftFraction.Localization.Q W).obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.MorphismProperty.LeftFraction.Localization.Q W).map s)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MorphismProperty.LeftFraction.Localization.Qinv s hs) h) =
    h
-- Mathlib.Algebra.Order.Group.Action.Flag
Flag.instSMulOrderIso : {α : Type u_1} → [inst : Preorder α] → SMul (α ≃o α) (Flag α)
-- Init.Data.List.Lemmas
List.map_filterMap : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → Option β} {g : β → γ} {l : List α},
  List.map g (List.filterMap f l) = List.filterMap (fun x => Option.map g (f x)) l
-- Mathlib.CategoryTheory.Dialectica.Monoidal
CategoryTheory.Dial.associator_naturality : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasFiniteProducts C]
  [inst_2 : CategoryTheory.Limits.HasPullbacks C] {X₁ X₂ X₃ Y₁ Y₂ Y₃ : CategoryTheory.Dial C} (f₁ : X₁ ⟶ Y₁)
  (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.tensorHom f₁ f₂) f₃)
      (CategoryTheory.MonoidalCategoryStruct.associator Y₁ Y₂ Y₃).hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X₁ X₂ X₃).hom
      (CategoryTheory.MonoidalCategoryStruct.tensorHom f₁ (CategoryTheory.MonoidalCategoryStruct.tensorHom f₂ f₃))
-- Mathlib.Data.Set.Lattice
Set.iUnion_true : ∀ {α : Type u_1} {s : True → Set α}, Set.iUnion s = s trivial
-- Mathlib.Algebra.MonoidAlgebra.Cardinal
/-- **Alias** of `MonoidAlgebra.cardinalMk_eq_max_lift_of_infinite`. -/
MonoidAlgebra.cardinalMk_lift_of_infinite : ∀ (R : Type u) (M' : Type v) [inst : Semiring R] [Infinite M'] [Nontrivial R],
  Cardinal.mk (MonoidAlgebra R M') = max (Cardinal.lift.{v, u} (Cardinal.mk R)) (Cardinal.lift.{u, v} (Cardinal.mk M'))
-- Std.Data.ExtDTreeMap.Basic
Std.ExtDTreeMap.instSingletonSigmaOfTransCmp : {α : Type u} →
  {β : α → Type v} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Singleton ((a : α) × β a) (Std.ExtDTreeMap α β cmp)
-- Std.Time.Format.Modifier
/-- Hour and minute without colon, with optional seconds (e.g., "+0130", "+013015")
 -/
Std.Time.OffsetZ.hourMinute : Std.Time.OffsetZ
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.RuleSets : Type
-- Mathlib.CategoryTheory.Limits.Preserves.Finite
CategoryTheory.Limits.PreservesFiniteProducts.preserves : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {D : Type u₂} {inst_1 : CategoryTheory.Category.{v₂, u₂} D}
  {F : CategoryTheory.Functor C D} [self : CategoryTheory.Limits.PreservesFiniteProducts F] (n : ℕ),
  CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete (Fin n)) F
-- Mathlib.LinearAlgebra.RootSystem.Irreducible
RootPairing.invtRootSubmodule.eq_1 : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N),
  P.invtRootSubmodule = ⨅ i, Module.End.invtSubmodule ↑(P.reflection i)
-- Std.Data.TreeMap.Slice
Std.TreeMap.toList_rcc : ∀ {α : Type u} {β : Type v} (cmp : autoParam (α → α → Ordering) Std.TreeMap.toList_rcc._auto_1) [Std.TransCmp cmp]
  {t : Std.TreeMap α β cmp} {lowerBound upperBound : α},
  Std.Slice.toList (Std.Rcc.Sliceable.mkSlice t lowerBound...=upperBound) =
    List.filter (fun e => decide ((cmp e.1 lowerBound).isGE = true ∧ (cmp e.1 upperBound).isLE = true)) t.toList
-- Mathlib.Algebra.Group.Submonoid.Basic
IsUnit.mem_submonoid_iff : ∀ {M : Type u_4} [inst : Monoid M] (a : M), a ∈ IsUnit.submonoid M ↔ IsUnit a
-- Mathlib.LinearAlgebra.Dimension.Basic
Module.one_le_rank_iff : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  1 ≤ Module.rank R M ↔ ∃ f, Function.Injective ⇑f
-- Mathlib.Data.Finset.Insert
Finset.prodPiInsert.congr_simp : ∀ {α : Type u_1} {inst : DecidableEq α} [inst_1 : DecidableEq α] {s : Finset α} (f : α → Type u_3) {a : α}
  (x x_1 : f a × ((i : α) → i ∈ s → f i)),
  x = x_1 → ∀ (i : α) (a_1 : i ∈ insert a s), Finset.prodPiInsert f x i a_1 = Finset.prodPiInsert f x_1 i ⋯
-- Mathlib.Analysis.FunctionalSpaces.SobolevInequality
MeasureTheory.GridLines.T.eq_1 : ∀ {ι : Type u_1} {A : ι → Type u_2} [inst : (i : ι) → MeasurableSpace (A i)] (μ : (i : ι) → MeasureTheory.Measure (A i))
  [inst_1 : DecidableEq ι] (p : ℝ) (f : ((i : ι) → A i) → ENNReal) (s : Finset ι),
  MeasureTheory.GridLines.T μ p f s = ∫⋯∫⁻_s, f ^ (1 - (↑s.card - 1) * p) * ∏ i ∈ s, (∫⋯∫⁻_{i}, f ∂μ) ^ p ∂μ
-- Mathlib.Algebra.Opposites
MulOpposite.op_eq_one_iff : ∀ {α : Type u_1} [inst : One α] (a : α), MulOpposite.op a = 1 ↔ a = 1
-- Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
hasDerivAt_jacobiTheta₂_fst : ∀ (z : ℂ) {τ : ℂ}, 0 < τ.im → HasDerivAt (fun x => jacobiTheta₂ x τ) (jacobiTheta₂' z τ) z
-- Mathlib.Order.DirSupClosed
DirSupInacc.univ : ∀ {α : Type u_1} [inst : Preorder α], DirSupInacc Set.univ
-- Mathlib.CategoryTheory.Shift.Basic
CategoryTheory.shiftFunctorAdd'_assoc_inv_app_assoc : ∀ {C : Type u} {A : Type u_1} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : AddMonoid A]
  [inst_2 : CategoryTheory.HasShift C A] (a₁ a₂ a₃ a₁₂ a₂₃ a₁₂₃ : A) (h₁₂ : a₁ + a₂ = a₁₂) (h₂₃ : a₂ + a₃ = a₂₃)
  (h₁₂₃ : a₁ + a₂ + a₃ = a₁₂₃) (X : C) {Z : C} (h : (CategoryTheory.shiftFunctor C a₁₂₃).obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.shiftFunctor C a₃).map ((CategoryTheory.shiftFunctorAdd' C a₁ a₂ a₁₂ h₁₂).inv.app X))
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd' C a₁₂ a₃ a₁₂₃ ⋯).inv.app X) h) =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.shiftFunctorAdd' C a₂ a₃ a₂₃ h₂₃).inv.app ((CategoryTheory.shiftFunctor C a₁).obj X))
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd' C a₁ a₂₃ a₁₂₃ ⋯).inv.app X) h)
-- Mathlib.NumberTheory.Padics.PadicVal.Basic
/-- The `p`-adic value of a natural is its `p`-adic value as an integer.  -/
padicValInt.of_nat : ∀ {p n : ℕ}, padicValInt p ↑n = padicValNat p n
-- Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite
Finset.prod_Ico_mul_eq_prod_Icc : ∀ {α : Type u_1} {M : Type u_2} [inst : CommMonoid M] {f : α → M} {a b : α} [inst_1 : PartialOrder α]
  [inst_2 : LocallyFiniteOrder α], a ≤ b → (∏ x ∈ Finset.Ico a b, f x) * f b = ∏ x ∈ Finset.Icc a b, f x
-- Mathlib.Data.Sum.Interval
Sum.Lex.Ioc_inl_inl : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : LocallyFiniteOrder α]
  [inst_3 : LocallyFiniteOrder β] [inst_4 : LocallyFiniteOrderTop α] [inst_5 : LocallyFiniteOrderBot β] (a₁ a₂ : α),
  Finset.Ioc (Sum.inlₗ a₁) (Sum.inlₗ a₂) =
    Finset.map (Function.Embedding.inl.trans toLex.toEmbedding) (Finset.Ioc a₁ a₂)
-- Mathlib.CategoryTheory.Limits.WeakLimits.Basic
/-- Transport evidence that a cone is a weak limit cone across an isomorphism of cones.  -/
CategoryTheory.Limits.IsWeakLimit.ofIsoWeakLimit : {J : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} J] →
    {C : Type u_3} →
      [inst_1 : CategoryTheory.Category.{v_3, u_3} C] →
        {F : CategoryTheory.Functor J C} →
          {r t : CategoryTheory.Limits.Cone F} →
            CategoryTheory.Limits.IsWeakLimit r → (r ≅ t) → CategoryTheory.Limits.IsWeakLimit t
-- Lean.Structure
/-- Caches a structure's resolution order.  -/
_private.Lean.Structure.0.Lean.setStructureResolutionOrder : {m : Type → Type} → [Lean.MonadEnv m] → Lean.Name → Array Lean.Name → m Unit
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Int
Int.reduceToNat : Lean.Meta.Simp.DSimproc
-- Mathlib.SetTheory.Cardinal.Finite
Function.Surjective.bijective_of_nat_card_le : ∀ {α : Type u_1} {β : Type u_2} [Finite α] {f : α → β},
  Function.Surjective f → Nat.card α ≤ Nat.card β → Function.Bijective f
-- Aesop.Nanos
Aesop.instBEqNanos.beq : Aesop.Nanos → Aesop.Nanos → Bool
-- Batteries.Data.HashMap.Basic
/-- Builds a `HashMap` from a list of key-value pairs.
Values of duplicated keys are replaced by their respective last occurrences.
```
ofList [("one", 1), ("one", 2)] = {"one" => 2}
```
 -/
Batteries.HashMap.ofList : {α : Type u_1} → {β : Type u_2} → [inst : BEq α] → [inst_1 : Hashable α] → List (α × β) → Batteries.HashMap α β
-- Mathlib.CategoryTheory.Limits.Shapes.Grothendieck
/-- A cocone on a functor `G : Grothendieck F ⥤ H` induces a cocone on the fiberwise colimit
on `G`.  -/
CategoryTheory.Limits.coconeFiberwiseColimitOfCocone : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {F : CategoryTheory.Functor C CategoryTheory.Cat} →
      {H : Type u₂} →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} H] →
          {G : CategoryTheory.Functor (CategoryTheory.Grothendieck F) H} →
            [inst_2 :
                ∀ {X Y : C} (f : X ⟶ Y),
                  CategoryTheory.Limits.HasColimit
                    ((F.map f).toFunctor.comp ((CategoryTheory.Grothendieck.ι F Y).comp G))] →
              CategoryTheory.Limits.Cocone G → CategoryTheory.Limits.Cocone (CategoryTheory.Limits.fiberwiseColimit G)
-- Mathlib.SetTheory.Cardinal.Cofinality.Basic
/-- Every well-order has a cofinal subset of cardinal `cof α`.  -/
Order.exists_cof_eq : ∀ (α : Type u) [inst : Preorder α], ∃ s, IsCofinal s ∧ Cardinal.mk ↑s = Order.cof α
-- Lean.ToExpr
Lean.instToExprRat : Lean.ToExpr ℚ
-- Mathlib.Algebra.Homology.HomologicalComplexBiprod
HomologicalComplex.biprod_inr_snd_f : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {c : ComplexShape ι} (K L : HomologicalComplex C c)
  [inst_2 : ∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (L.X i)] (i : ι),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.inr.f i) (CategoryTheory.Limits.biprod.snd.f i) =
    CategoryTheory.CategoryStruct.id (L.X i)
-- Mathlib.Data.EReal.Operations
EReal.neg_pos : ∀ {a : EReal}, 0 < -a ↔ a < 0
-- Mathlib.Data.Finset.NAry
Finset.image₂_union_inter_subset : ∀ {α : Type u_1} {β : Type u_3} [inst : DecidableEq α] [inst_1 : DecidableEq β] {f : α → α → β} {s t : Finset α},
  (∀ (a b : α), f a b = f b a) → Finset.image₂ f (s ∪ t) (s ∩ t) ⊆ Finset.image₂ f s t
-- Mathlib.RingTheory.DedekindDomain.Factorization
/-- Let `I J I' J'` be nonzero fractional ideals in a Dedekind domain with `J ≤ I` and `J' ≤ I'`.
If `I/J = I'/J'` in the group of fractional ideals (i.e. `I * J' = I' * J`),
then `I/J ≃ I'/J'` as quotient `R`-modules.  -/
FractionalIdeal.quotientEquiv : {R : Type u_1} →
  [inst : CommRing R] →
    {K : Type u_2} →
      [inst_1 : Field K] →
        [inst_2 : Algebra R K] →
          [IsFractionRing R K] →
            [IsDedekindDomain R] →
              (I J I' J' : FractionalIdeal (nonZeroDivisors R) K) →
                I * J' = I' * J →
                  J ≤ I →
                    J' ≤ I' →
                      J' ≠ 0 →
                        I ≠ 0 → (↥↑I ⧸ Submodule.comap (↑I).subtype ↑J) ≃ₗ[R] ↥↑I' ⧸ Submodule.comap (↑I').subtype ↑J'
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Cases.alts : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.Cases pu → Array (Lean.Compiler.LCNF.Alt pu)
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.monadLift_OptionT : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {α : Type u} [inst : Monad m] [inst_1 : Std.Do.WPMonad m ps] (x : m α)
  (Q : Std.Do.PostCond α (Std.Do.PostShape.except PUnit.{u + 1} ps)),
  ⦃(Std.Do.wp x).apply (fun a => Q.1 a, Q.2.2)⦄ MonadLift.monadLift x ⦃Q⦄
-- Init.Prelude
/-- `.num p v` is now the preferred form.
 -/
Lean.Name.mkNum : Lean.Name → ℕ → Lean.Name
-- Mathlib.Topology.ContinuousMap.ContinuousMapZero
ContinuousMapZero.nonUnitalStarAlgHom_precomp_apply : ∀ {X : Type u_1} {Y : Type u_2} (R : Type u_4) [inst : Zero X] [inst_1 : Zero Y] [inst_2 : TopologicalSpace X]
  [inst_3 : TopologicalSpace Y] [inst_4 : TopologicalSpace R] [inst_5 : CommSemiring R] [inst_6 : StarRing R]
  [inst_7 : IsTopologicalSemiring R] [inst_8 : ContinuousStar R] (f : ContinuousMapZero X Y)
  (g : ContinuousMapZero Y R), (ContinuousMapZero.nonUnitalStarAlgHom_precomp R f) g = g.comp f