mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Grind.Ring.CommSolver
_private.Init.Grind.Ring.CommSolver.0.Lean.Grind.CommRing.Expr.toPoly.match_4.eq_3 : ∀ (motive : Lean.Grind.CommRing.Expr → Sort u_1) (k : ℕ) (h_1 : (k : ℤ) → motive (Lean.Grind.CommRing.Expr.num k))
  (h_2 : (k : ℤ) → motive (Lean.Grind.CommRing.Expr.intCast k))
  (h_3 : (k : ℕ) → motive (Lean.Grind.CommRing.Expr.natCast k))
  (h_4 : (x : Lean.Grind.CommRing.Var) → motive (Lean.Grind.CommRing.Expr.var x))
  (h_5 : (a b : Lean.Grind.CommRing.Expr) → motive (a.add b))
  (h_6 : (a b : Lean.Grind.CommRing.Expr) → motive (a.mul b)) (h_7 : (a : Lean.Grind.CommRing.Expr) → motive a.neg)
  (h_8 : (a b : Lean.Grind.CommRing.Expr) → motive (a.sub b))
  (h_9 : (a : Lean.Grind.CommRing.Expr) → (k : ℕ) → motive (a.pow k)),
  (match Lean.Grind.CommRing.Expr.natCast k with
    | Lean.Grind.CommRing.Expr.num k => h_1 k
    | Lean.Grind.CommRing.Expr.intCast k => h_2 k
    | Lean.Grind.CommRing.Expr.natCast k => h_3 k
    | Lean.Grind.CommRing.Expr.var x => h_4 x
    | a.add b => h_5 a b
    | a.mul b => h_6 a b
    | a.neg => h_7 a
    | a.sub b => h_8 a b
    | a.pow k => h_9 a k) =
    h_3 k
-- Std.Http.Data.Headers.Basic
Std.Http.Header.ContentLength.mk.sizeOf_spec : ∀ (length : ℕ), sizeOf { length := length } = 1 + sizeOf length
-- Mathlib.Topology.MetricSpace.Pseudo.Pi
nndist_le_pi_nndist : ∀ {β : Type u_2} {X : β → Type u_3} [inst : Fintype β] [inst_1 : (b : β) → PseudoMetricSpace (X b)]
  (f g : (b : β) → X b) (b : β), nndist (f b) (g b) ≤ nndist f g
-- Std.Tactic.BVDecide.Normalize.BitVec
Std.Tactic.BVDecide.Normalize.Int16.toBitVec_cond : ∀ {c : Bool} {t e : Int16}, (bif c then t else e).toBitVec = bif c then t.toBitVec else e.toBitVec
-- Mathlib.GroupTheory.GroupAction.Blocks
MulAction.IsTrivialBlock.image : ∀ {M : Type u_3} {α : Type u_4} {N : Type u_5} {β : Type u_6} [inst : Monoid M] [inst_1 : MulAction M α]
  [inst_2 : Monoid N] [inst_3 : MulAction N β] {φ : M → N} {f : α →ₑ[φ] β},
  Function.Surjective ⇑f → ∀ {B : Set α}, MulAction.IsTrivialBlock B → MulAction.IsTrivialBlock (⇑f '' B)
-- Mathlib.Algebra.Lie.Derivation.Basic
LieDerivation.instSMulInt : ∀ {L : Type u_2} {M : Type u_3} [inst : LieRing L] [inst_1 : AddCommGroup M] [inst_2 : LieRingModule L M],
  LieDerivation.SMulBracketCommClass ℤ L M
-- Mathlib.Order.Hom.Bounded
OrderIsoClass.toTopHomClass : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : EquivLike F α β] [inst_1 : LE α] [inst_2 : OrderTop α]
  [inst_3 : PartialOrder β] [inst_4 : OrderTop β] [OrderIsoClass F α β], TopHomClass F α β
-- Mathlib.AlgebraicTopology.SimplicialObject.Homotopy
CategoryTheory.SimplicialObject.Homotopy.precomp_h : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : CategoryTheory.SimplicialObject C} {f g : X ⟶ Y}
  (H : CategoryTheory.SimplicialObject.Homotopy f g) {X' : CategoryTheory.SimplicialObject C} (p : X' ⟶ X) {n : ℕ}
  (i : Fin (n + 1)), (H.precomp p).h i = CategoryTheory.CategoryStruct.comp (p.app (Opposite.op { len := n })) (H.h i)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get_insertManyIfNewUnit_list : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α fun x => Unit} {l : List α} {k : α}
  {h : k ∈ Std.DHashMap.Const.insertManyIfNewUnit m l},
  Std.DHashMap.Const.get (Std.DHashMap.Const.insertManyIfNewUnit m l) k h = ()
-- Mathlib.MeasureTheory.VectorMeasure.Prod
MeasureTheory.VectorMeasure.prod_apply_eq_integral : ∀ {X : Type u_2} {Y : Type u_3} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X}
  {mY : MeasurableSpace Y} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G] [inst_5 : NormedSpace ℝ G]
  {μ : MeasureTheory.VectorMeasure X E} {ν : MeasureTheory.VectorMeasure Y F} {B : E →L[ℝ] F →L[ℝ] G} [CompleteSpace G]
  [MeasureTheory.IsFiniteMeasure μ.variation] {s : Set (X × Y)},
  MeasurableSet s → (μ.prod ν B) s = ∫ᵛ (x : X), ν (Prod.mk x ⁻¹' s) ∂[B.flip; μ]
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.Equiv.getKey!_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α] {k : α}, t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.getKey! k = t₂.getKey! k
-- Mathlib.Data.Multiset.DershowitzManna
_private.Mathlib.Data.Multiset.DershowitzManna.0.Multiset.isDershowitzMannaLT_of_oneStep : ∀ {α : Type u_1} [inst : Preorder α] {M N : Multiset α}, Multiset.OneStep✝ M N → M.IsDershowitzMannaLT N
-- Std.Async.Select
_private.Std.Async.Select.0.Std.Async.Waiter.mk.injEq : ∀ {α : Type} (finished : IO.Ref Bool) (promise : IO.Promise (Except IO.Error α)) (finished_1 : IO.Ref Bool)
  (promise_1 : IO.Promise (Except IO.Error α)),
  ({ finished := finished, promise := promise } = { finished := finished_1, promise := promise_1 }) =
    (finished = finished_1 ∧ promise = promise_1)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
/-- Given three morphisms `f₁ : X₁ ⟶ S`, `f₂ : X₂ ⟶ S` and `f₃ : X₃ ⟶ S`, and chosen
pullbacks for `(f₁, f₂)`, `(f₂, f₃)` and `(f₁, f₃)`, this structure contains the data
of a wide pullback of the three morphisms `f₁`, `f₂` and `f₃`.  -/
CategoryTheory.Limits.ChosenPullback₃ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X₁ X₂ X₃ S : C} →
      {f₁ : X₁ ⟶ S} →
        {f₂ : X₂ ⟶ S} →
          {f₃ : X₃ ⟶ S} →
            CategoryTheory.Limits.ChosenPullback f₁ f₂ →
              CategoryTheory.Limits.ChosenPullback f₂ f₃ → CategoryTheory.Limits.ChosenPullback f₁ f₃ → Type (max u v)
-- Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare
/-- If `f : 𝕜 → E`, `𝕜 = ℝ` or `𝕜 = ℂ`, is differentiable on a convex set `s`,
then it admits a primitive.  -/
Convex.exists_forall_hasDerivWithinAt : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  [CompleteSpace E] {f : 𝕜 → E} {s : Set 𝕜},
  Convex ℝ s → DifferentiableOn 𝕜 f s → ∃ g, ∀ a ∈ s, HasDerivWithinAt g (f a) s a
-- Lean.Message
Lean.MessageLog.add : Lean.Message → Lean.MessageLog → Lean.MessageLog
-- Batteries.Recycling.MonadSatisfying.Basic
/-- `SatisfiesM` distributes over `pure`, general version / weakest precondition version.  -/
SatisfiesM.pure : ∀ {m : Type u_1 → Type u_2} {α : Type u_1} {p : α → Prop} {a : α} [inst : Applicative m] [LawfulApplicative m],
  p a → SatisfiesM p (pure a)
-- Mathlib.GroupTheory.IndexNSmul
/-- The relative index in `S` of the image of the multiplication-by-`n` map
on an additive subgroup `S` of an additive group such that `S` is free
and finitely generated as a `ℤ`-module is `n ^ finrank ℤ S`.  -/
AddSubgroup.relIndex_map_nsmul : ∀ {M : Type u_1} [inst : AddCommGroup M] (n : ℕ) (S : AddSubgroup M) [Module.Free ℤ ↥(AddSubgroup.toIntSubmodule S)]
  [Module.Finite ℤ ↥(AddSubgroup.toIntSubmodule S)],
  (AddSubgroup.map (nsmulAddMonoidHom n) S).relIndex S = n ^ Module.finrank ℤ ↥S
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.NumDenSameDeg.num_neg : ∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : NegMemClass σ A]
  {𝒜 : ι → σ} (x : Submonoid A) (c : HomogeneousLocalization.NumDenSameDeg 𝒜 x), ↑(-c).num = -↑c.num
-- Mathlib.Algebra.Module.Equiv.Defs
/-- `M ≃ₛₗ[σ] M₂` denotes the type of linear equivalences between `M` and `M₂` over a
ring homomorphism `σ`.  -/
«term_≃ₛₗ[_]_» : Lean.TrailingParserDescr
-- Mathlib.RingTheory.Valuation.Archimedean
Valuation.Integers.isPrincipalIdealRing_iff_not_denselyOrdered_mrange : ∀ {F : Type u_1} {Γ₀ : Type u_2} {O : Type u_3} [inst : Field F] [inst_1 : LinearOrderedCommGroupWithZero Γ₀]
  [inst_2 : CommRing O] [inst_3 : Algebra O F] {v : Valuation F Γ₀} [MulArchimedean ↥(MonoidHom.mrange v)],
  v.Integers O → (IsPrincipalIdealRing O ↔ ¬DenselyOrdered ↥(MonoidHom.mrange v))
-- Lean.Meta.Tactic.Simp.Main
_private.Lean.Meta.Tactic.Simp.Main.0.Lean.Meta.Simp.isMatchDef.go : Lean.Environment → Lean.Expr → Bool
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.contains_minKeyD : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp],
  t.isEmpty = false → ∀ {fallback : α}, t.contains (t.minKeyD fallback) = true
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.coe_comap : ∀ {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] (f : R →+* S) (s : Subsemiring S),
  ↑(Subsemiring.comap f s) = ⇑f ⁻¹' ↑s
-- Init.Data.List.Sublist
List.eq_nil_of_suffix_nil : ∀ {α : Type u_1} {l : List α}, l <:+ [] → l = []
-- Mathlib.Topology.UniformSpace.UniformEmbedding
IsUniformInducing.basis_uniformity : ∀ {α : Type u} {β : Type v} [inst : UniformSpace α] [inst_1 : UniformSpace β] {f : α → β},
  IsUniformInducing f →
    ∀ {ι : Sort u_1} {p : ι → Prop} {s : ι → Set (β × β)},
      (uniformity β).HasBasis p s → (uniformity α).HasBasis p fun i => Prod.map f f ⁻¹' s i
-- Mathlib.Data.Set.Finite.Lattice
iInf_iSup_of_monotone : ∀ {ι : Type u_1} {ι' : Type u_2} {α : Type u_3} [Finite ι] [inst : Preorder ι'] [Nonempty ι'] [IsCodirectedOrder ι']
  [inst_3 : Order.Coframe α] {f : ι → ι' → α}, (∀ (i : ι), Monotone (f i)) → ⨅ j, ⨆ i, f i j = ⨆ i, ⨅ j, f i j
-- Mathlib.Algebra.Algebra.RestrictScalars
RestrictScalars.addEquiv_map_smul : ∀ (R : Type u_1) (S : Type u_2) (M : Type u_3) [inst : AddCommMonoid M] [inst_1 : CommSemiring R] [inst_2 : Semiring S]
  [inst_3 : Algebra R S] [inst_4 : Module S M] (c : R) (x : RestrictScalars R S M),
  (RestrictScalars.addEquiv R S M) (c • x) = (algebraMap R S) c • (RestrictScalars.addEquiv R S M) x
-- Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ
/-- The Weierstrass curve `Y² + Y = X³`. It is of j-invariant 0 if it is an elliptic curve.  -/
WeierstrassCurve.ofJ0 : (R : Type u_1) → [CommRing R] → WeierstrassCurve R
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
mul_self_lt_mul_self_iff : ∀ {R : Type u} [inst : Semiring R] [inst_1 : LinearOrder R] [PosMulStrictMono R] [MulPosMono R] {a b : R},
  0 ≤ a → 0 ≤ b → (a < b ↔ a * a < b * b)
-- Mathlib.Algebra.Order.Ring.Abs
sq_le_one_iff_abs_le_one : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] (a : α), a ^ 2 ≤ 1 ↔ |a| ≤ 1
-- Mathlib.Combinatorics.SimpleGraph.Copy
/-- **Alias** of `SimpleGraph.bot_isContained_iff_card_le`.

---

`⊥` is contained in any simple graph having sufficiently many vertices.  -/
SimpleGraph.IsContained.bot : ∀ {α : Type u_4} {β : Type u_5} {B : SimpleGraph β} [inst : Fintype α] [inst_1 : Fintype β],
  ⊥.IsContained B ↔ Fintype.card α ≤ Fintype.card β
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
/-- The left-hand side of `sum_ite_self_eq` simplifies; this is the variant that is useful for `simp`.
 -/
Finsupp.if_mem_support : ∀ {α : Type u_1} [inst : DecidableEq α] {N : Type u_16} [inst_1 : Zero N] (f : α →₀ N) (a : α),
  (if a ∈ f.support then f a else 0) = f a
-- Mathlib.FieldTheory.NormalizedTrace
Algebra.normalizedTrace.congr_simp : ∀ (F : Type u_1) (K : Type u_2) [inst : Field F] [inst_1 : Field K] [inst_2 : Algebra F K] [inst_3 : CharZero F]
  [inst_4 : Algebra.IsIntegral F K], Algebra.normalizedTrace F K = Algebra.normalizedTrace F K
-- Mathlib.RingTheory.Spectrum.Prime.RingHom
PrimeSpectrum.comap_asIdeal : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : CommSemiring S] (f : R →+* S) (y : PrimeSpectrum S),
  (PrimeSpectrum.comap f y).asIdeal = Ideal.comap f y.asIdeal
-- Mathlib.Data.Vector.Basic
List.Vector.mOfFn.eq_1 : ∀ {m : Type u → Type u_6} [inst : Monad m] {α : Type u} (x_2 : Fin 0 → m α),
  List.Vector.mOfFn x_2 = pure List.Vector.nil
-- Init.Data.String.Iterate
/-- Creates an iterator over all valid positions within {name}`s`.

Examples:
* {lean}`("abc".toSlice.positions.map (fun ⟨p, h⟩ => p.get h) |>.toList) = ['a', 'b', 'c']`
* {lean}`("abc".toSlice.positions.map (·.val.offset.byteIdx) |>.toList) = [0, 1, 2]`
* {lean}`("ab∀c".toSlice.positions.map (fun ⟨p, h⟩ => p.get h) |>.toList) = ['a', 'b', '∀', 'c']`
* {lean}`("ab∀c".toSlice.positions.map (·.val.offset.byteIdx) |>.toList) = [0, 1, 2, 5]`
 -/
String.Slice.positions : (s : String.Slice) → Std.Iter { p // p ≠ s.endPos }
-- Mathlib.Data.Finset.PImage
Part.toFinset_none : ∀ {α : Type u_1} [inst : Decidable Part.none.Dom], Part.none.toFinset = ∅
-- Lean.Meta.Tactic.Grind.AC.Util
Lean.Meta.Grind.AC.ACM.Context.mk : ℕ → Lean.Meta.Grind.AC.ACM.Context
-- Mathlib.Analysis.LocallyConvex.WeakDual
LinearMap.toSeminorm_ball_zero : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E] {f : E →ₗ[𝕜] 𝕜}
  {r : ℝ}, f.toSeminorm.ball 0 r = {x | ‖f x‖ < r}
-- Mathlib.MeasureTheory.Integral.Bochner.L1
MeasureTheory.SimpleFunc.posPart_sub_negPart : ∀ {α : Type u_1} [inst : MeasurableSpace α] (f : MeasureTheory.SimpleFunc α ℝ), f.posPart - f.negPart = f
-- Mathlib.Data.Set.MulAntidiagonal
Set.AddAntidiagonal.fst_eq_fst_iff_snd_eq_snd : ∀ {α : Type u_1} [inst : AddCommMonoid α] [IsCancelAdd α] {s t : Set α} {a : α} {x y : ↑(s.antidiagonal t a)},
  (↑x).1 = (↑y).1 ↔ (↑x).2 = (↑y).2
-- Mathlib.CategoryTheory.Discrete.Basic
/-- Any function `I → C` gives a functor `Discrete I ⥤ C`.  -/
CategoryTheory.Discrete.functor : {C : Type u₂} →
  [inst : CategoryTheory.Category.{v₂, u₂} C] →
    {I : Type u₁} → (I → C) → CategoryTheory.Functor (CategoryTheory.Discrete I) C
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.Monic.ne_zero_of_polynomial_ne : ∀ {R : Type u} [inst : Semiring R] {p q r : Polynomial R}, p.Monic → q ≠ r → p ≠ 0
-- Mathlib.Data.Seq.Basic
Stream'.Seq.get?_set_of_not_terminatedAt : ∀ {α : Type u} (x : α) {s : Stream'.Seq α} {n : ℕ}, ¬s.TerminatedAt n → (s.set n x).get? n = some x
-- Mathlib.Topology.Algebra.Group.Basic
/-- Conjugation acting on fixed element of the group is continuous when both `mul` and
`inv` are continuous.  -/
IsTopologicalGroup.continuous_conj' : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Inv G] [inst_2 : Mul G] [ContinuousMul G] [ContinuousInv G]
  (h : G), Continuous fun g => g * h * g⁻¹
-- Mathlib.MeasureTheory.OuterMeasure.Basic
MeasureTheory.measure_iUnion_null_iff : ∀ {α : Type u_1} {F : Type u_3} [inst : FunLike F (Set α) ENNReal] [MeasureTheory.OuterMeasureClass F α] {μ : F}
  {ι : Sort u_4} [Countable ι] {s : ι → Set α}, μ (⋃ i, s i) = 0 ↔ ∀ (i : ι), μ (s i) = 0
-- Mathlib.CategoryTheory.Monoidal.Mon
/-- The unit morphism of a monoid object.  -/
CategoryTheory.MonObj.one : {C : Type u₁} →
  {inst : CategoryTheory.Category.{v₁, u₁} C} →
    {inst_1 : CategoryTheory.MonoidalCategory C} →
      {X : C} → [self : CategoryTheory.MonObj X] → CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ X
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
groupCohomology.H2π_comp_map : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u, u, u} k H}
  {B : Rep.{u, u, u} k G} (f : G →* H) (φ : Rep.res f A ⟶ B),
  CategoryTheory.CategoryStruct.comp (groupCohomology.H2π A) (groupCohomology.map f φ 2) =
    CategoryTheory.CategoryStruct.comp (groupCohomology.mapCocycles₂ f φ) (groupCohomology.H2π B)
-- Mathlib.FieldTheory.PerfectClosure
PerfectClosure.instCommRing : (K : Type u) →
  [inst : CommRing K] → (p : ℕ) → [inst_1 : Fact (Nat.Prime p)] → [inst_2 : CharP K p] → CommRing (PerfectClosure K p)
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
MeasureTheory.condExp_bot_ae_eq : ∀ {α : Type u_1} {E : Type u_3} {m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [CompleteSpace E] (f : α → E),
  μ[f | ⊥] =ᵐ[μ] fun x => (μ.real Set.univ)⁻¹ • ∫ (x : α), f x ∂μ
-- Mathlib.Data.Set.Prod
range_toPullbackDiag : ∀ {X : Type u_1} {Y : Sort u_2} (f : X → Y), Set.range (toPullbackDiag f) = Function.pullbackDiagonal f
-- Init.Data.Int.Gcd
Int.lcm_mul_left_dvd_mul_lcm : ∀ (k m n : ℕ), (↑m * ↑n).lcm ↑k ∣ (↑m).lcm ↑k * (↑n).lcm ↑k
-- Mathlib.MeasureTheory.Group.Prod
MeasureTheory.measurable_measure_add_right : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : AddGroup G] [MeasurableAdd₂ G] (μ : MeasureTheory.Measure G)
  [MeasureTheory.SFinite μ] {s : Set G}, MeasurableSet s → Measurable fun x => μ ((fun y => y + x) ⁻¹' s)
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rco.size_eq_if_rcc : ∀ {α : Type u} {r : Std.Rco α} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.Rxo.HasSize α] [Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLT α]
  [Std.Rxo.IsAlwaysFinite α] [Std.Rxo.LawfulHasSize α],
  r.size =
    if r.lower < r.upper then
      match Std.PRange.succ? r.lower with
      | none => 1
      | some next => (next...r.upper).size + 1
    else 0
-- Mathlib.SetTheory.Cardinal.Cofinality.Club
IsStationary.eq_1 : ∀ {α : Type v} [inst : LinearOrder α] (s : Set α), IsStationary s = ∀ ⦃t : Set α⦄, IsClub t → (s ∩ t).Nonempty
-- Mathlib.Combinatorics.Matroid.Rank.ENat
Matroid.eRk_eq_one_iff : ∀ {α : Type u_1} {M : Matroid α} {X : Set α},
  autoParam (X ⊆ M.E) Matroid.eRk_eq_one_iff._auto_1 → (M.eRk X = 1 ↔ ∃ e ∈ X, M.IsNonloop e ∧ X ⊆ M.closure {e})
-- Mathlib.Algebra.Group.Submonoid.Membership
/-- The submonoid generated by an element is a group if that element has finite order.  -/
Submonoid.groupPowers : {M : Type u_1} → [inst : Monoid M] → {x : M} → {n : ℕ} → 0 < n → x ^ n = 1 → Group ↥(Submonoid.powers x)
-- Std.Time.Date.Basic
/-- Convert `Minute.Offset` into `Week.Offset`.
 -/
Std.Time.Minute.Offset.toWeeks : Std.Time.Minute.Offset → Std.Time.Week.Offset
-- Mathlib.Algebra.Group.Hom.Defs
/-- If `f` is a monoid homomorphism then `f 1 = 1`.  -/
MonoidHom.map_one : ∀ {M : Type u_4} {N : Type u_5} [inst : MulOne M] [inst_1 : MulOne N] (f : M →* N), f 1 = 1
-- Mathlib.LinearAlgebra.SymplecticGroup
/-- Symplectic matrices over a local ring have determinant 1.  -/
_private.Mathlib.LinearAlgebra.SymplecticGroup.0.SymplecticGroup.det_eq_one_of_isLocalRing : ∀ {l : Type u_1} {R : Type u_2} [inst : DecidableEq l] [inst_1 : Fintype l] [inst_2 : CommRing R] [IsLocalRing R]
  {M : Matrix (l ⊕ l) (l ⊕ l) R}, M ∈ Matrix.symplecticGroup l R → M.det = 1
-- Mathlib.NumberTheory.Harmonic.ZetaAsymp
/-- **Alias** of `ZetaAsymptotics.termTSum_of_lt`.

---

For `1 < s`, the topological sum of `ZetaAsymptotics.term (n + 1) s` over all `n : ℕ` is
`1 / (s - 1) - ζ s / s`.
 -/
ZetaAsymptotics.term_tsum_of_lt : ∀ {s : ℝ}, 1 < s → ZetaAsymptotics.termTSum s = 1 / (s - 1) - 1 / s * ∑' (n : ℕ), 1 / (↑n + 1) ^ s
-- Init.Prelude
/-- The class `OfNat α n` powers the numeric literal parser. If you write
`37 : α`, Lean will attempt to synthesize `OfNat α 37`, and will generate
the term `(OfNat.ofNat 37 : α)`.

There is a bit of infinite regress here since the desugaring apparently
still contains a literal `37` in it. The type of expressions contains a
primitive constructor for "raw natural number literals", which you can directly
access using the macro `nat_lit 37`. Raw number literals are always of type `Nat`.
So it would be more correct to say that Lean looks for an instance of
`OfNat α (nat_lit 37)`, and it generates the term `(OfNat.ofNat (nat_lit 37) : α)`.
 -/
OfNat : Type u → ℕ → Type u
-- Mathlib.Algebra.Order.AbsoluteValue.Basic
IsAbsoluteValue.sub_abv_le_abv_sub : ∀ {S : Type u_5} [inst : Ring S] [inst_1 : PartialOrder S] {R : Type u_6} [inst_2 : Ring R] (abv : R → S)
  [IsAbsoluteValue abv] [IsOrderedRing S] (a b : R), abv a - abv b ≤ abv (a - b)
-- Mathlib.CategoryTheory.Triangulated.Triangulated
CategoryTheory.Triangulated.Octahedron.comm₃ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃}
  {comm : CategoryTheory.CategoryStruct.comp u₁₂ u₂₃ = u₁₃} {v₁₂ : X₂ ⟶ Z₁₂}
  {w₁₂ : Z₁₂ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁}
  {h₁₂ : CategoryTheory.Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  {v₂₃ : X₃ ⟶ Z₂₃} {w₂₃ : Z₂₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₂}
  {h₂₃ : CategoryTheory.Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  {v₁₃ : X₃ ⟶ Z₁₃} {w₁₃ : Z₁₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁}
  {h₁₃ : CategoryTheory.Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  (self : CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃), CategoryTheory.CategoryStruct.comp v₁₃ self.m₃ = v₂₃
-- Mathlib.Topology.Algebra.Group.ClosedSubgroup
AddSubgroup.normalCore_isClosed : ∀ {G : Type u} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [SeparatelyContinuousAdd G] (H : AddSubgroup G),
  IsClosed ↑H → IsClosed ↑H.normalCore
-- Std.Data.Internal.List.Associative
Std.Internal.List.getEntry?_eraseKey_of_false : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k a : α},
  (k == a) = false → Std.Internal.List.getEntry? a (Std.Internal.List.eraseKey k l) = Std.Internal.List.getEntry? a l
-- Mathlib.Topology.OpenPartialHomeomorph.Defs
OpenPartialHomeomorph.left_inv : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y) {x : X}, x ∈ e.source → ↑e.symm (↑e x) = x
-- Lean.Meta.Tactic.Grind.Types
/-- Returns the root of the congruence class containing `e`.  -/
Lean.Meta.Grind.getCongrRoot : Lean.Expr → Lean.Meta.Grind.GoalM Lean.Expr
-- Batteries.Data.List.Basic
List.takeListTR.go.eq_2 : ∀ {α : Type u_1} (a : List α) (a_1 : Array (List α)) (n : ℕ) (ns : List ℕ),
  List.takeListTR.go (n :: ns) a a_1 =
    match List.splitAt n a with
    | (xs₁, xs₂) => List.takeListTR.go ns xs₂ (a_1.push xs₁)
-- Mathlib.Tactic.Ring.Common
/-- Cast `ExBaseNat` to `ExBase btℕ sℕ`.  -/
Mathlib.Tactic.Ring.Common.ExBaseNat.toExBase : (e : Q(ℕ)) →
  Mathlib.Tactic.Ring.Common.ExBaseNat e →
    (e' : Q(ℕ)) × Mathlib.Tactic.Ring.Common.ExBase Mathlib.Tactic.Ring.Common.btℕ Mathlib.Tactic.Ring.Common.sℕ e'
-- Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling
/-- Convenience function to get the color of the edge `x ~ y` in the coloring of the complete graph
on `V`.
 -/
SimpleGraph.EdgeLabeling.get : {V : Type u_1} → {G : SimpleGraph V} → {K : Type u_3} → G.EdgeLabeling K → (x y : V) → G.Adj x y → K
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.Nonempty.zpow : ∀ {α : Type u_2} [inst : DivisionMonoid α] {s : Set α}, s.Nonempty → ∀ {n : ℤ}, (s ^ n).Nonempty
-- Mathlib.MeasureTheory.Measure.AddContent
MeasureTheory.AddContent.sUnion' : ∀ {α : Type u_1} {G : Type u_2} [inst : AddCommMonoid G] {C : Set (Set α)} (self : MeasureTheory.AddContent G C)
  (I : Finset (Set α)), ↑I ⊆ C → (↑I).PairwiseDisjoint id → ⋃₀ ↑I ∈ C → self.toFun (⋃₀ ↑I) = ∑ u ∈ I, self.toFun u
-- Mathlib.Analysis.Normed.Operator.Fredholm.Basic
/-- A `FredholmDecomposition` of the domain.  -/
ContinuousLinearMap.FredholmPackage.decDom : {𝕜 : Type u_1} →
  {E : Type u_2} →
    {F : Type u_3} →
      [inst : NontriviallyNormedField 𝕜] →
        [inst_1 : AddCommGroup E] →
          [inst_2 : AddCommGroup F] →
            [inst_3 : Module 𝕜 E] →
              [inst_4 : Module 𝕜 F] →
                [inst_5 : TopologicalSpace E] →
                  [inst_6 : TopologicalSpace F] → {u : E →L[𝕜] F} → u.FredholmPackage → FredholmDecomposition 𝕜 E
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.mkIso_inv_fst : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {X : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} X] {S S' : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X}
  (eₗ : S.fst ≅ S'.fst) (eᵣ : S.snd ≅ S'.snd)
  (w :
    autoParam
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight eₗ.hom F) S'.iso.hom =
        CategoryTheory.CategoryStruct.comp S.iso.hom (CategoryTheory.Functor.whiskerRight eᵣ.hom G))
      CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.mkIso._auto_1),
  (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.mkIso eₗ eᵣ w).inv.fst = eₗ.inv