mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.Measure.ae_eval_ne : ∀ {ι : Type u_1} {α : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → MeasurableSpace (α i)]
  (μ : (i : ι) → MeasureTheory.Measure (α i)) [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)] (i : ι)
  [MeasureTheory.NullSingletonClass (μ i)] (x : α i), ∀ᵐ (y : (i : ι) → α i) ∂MeasureTheory.Measure.pi μ, y i ≠ x
-- Lean.Server.InfoUtils
/-- Whether the tactic info is further indented than the hover position.  -/
Lean.Elab.GoalsAtResult.indented : Lean.Elab.GoalsAtResult → Bool
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsLittleO.add_add : ∀ {α : Type u_1} {E' : Type u_6} {F' : Type u_7} [inst : SeminormedAddCommGroup E'] [inst_1 : SeminormedAddCommGroup F']
  {l : Filter α} {f₁ f₂ : α → E'} {g₁ g₂ : α → F'},
  f₁ =o[l] g₁ → f₂ =o[l] g₂ → (fun x => f₁ x + f₂ x) =o[l] fun x => ‖g₁ x‖ + ‖g₂ x‖
-- Mathlib.Algebra.Group.Defs
neg_add_cancel : ∀ {G : Type u_1} [inst : AddGroup G] (a : G), -a + a = 0
-- Mathlib.RingTheory.DividedPowers.SubDPIdeal
/-- Divided powers on the quotient are compatible with quotient map  -/
DividedPowers.Quotient.dpow_apply : ∀ {A : Type u_1} [inst : CommRing A] {I : Ideal A} (hI : DividedPowers I) {J : Ideal A} (hIJ : hI.IsSubDPIdeal (J ⊓ I))
  {n : ℕ} {a : A},
  a ∈ I →
    (DividedPowers.Quotient.dividedPowers hI hIJ).dpow n ((Ideal.Quotient.mk J) a) = (Ideal.Quotient.mk J) (hI.dpow n a)
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
/-- The refinement given by restricting the indexing type.  -/
CategoryTheory.PreZeroHypercover.restrictIndexHom : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {S : C} → (E : CategoryTheory.PreZeroHypercover S) → {ι : Type w'} → (f : ι → E.I₀) → (E.restrictIndex f).Hom E
-- Init.Data.Iterators.Lemmas.Combinators.Attach
Std.Iter.unattach_toListRev_attachWith : ∀ {α β : Type u_1} {P : β → Prop} [inst : Std.Iterator α Id β] {it : Std.Iter β}
  {hP : ∀ (out : β), it.IsPlausibleIndirectOutput out → P out} [Std.Iterators.Finite α Id],
  (it.attachWith P hP).toListRev.unattach = it.toListRev
-- Mathlib.Data.QPF.Multivariate.Constructions.Cofix
MvQPF.Cofix.mk.eq_1 : ∀ {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n},
  MvQPF.Cofix.mk = MvQPF.Cofix.corec fun x => MvFunctor.map (TypeVec.id ::: fun i => i.dest) x
-- Mathlib.Algebra.Category.Grp.EpiMono
AddGrpCat.epi_iff_range_eq_top : ∀ {A B : AddGrpCat} (f : A ⟶ B), CategoryTheory.Epi f ↔ (AddGrpCat.Hom.hom f).range = ⊤
-- Lean.PrettyPrinter.Delaborator.Builtins
/-- A regular argument that, if it comes as the last argument, may be omitted.  -/
Lean.PrettyPrinter.Delaborator.AppImplicitArg.optional : Lean.Name → Lean.Term → Lean.PrettyPrinter.Delaborator.AppImplicitArg
-- Init.Grind.Ring.Envelope
Lean.Grind.Ring.OfSemiring.r_rfl : ∀ {α : Type u} [inst : Lean.Grind.Semiring α] (a : α × α), Lean.Grind.Ring.OfSemiring.r α a a
-- Mathlib.FieldTheory.Finiteness
IsNoetherian.coe_finsetBasisIndex : ∀ (K : Type u) (V : Type v) [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  [inst_3 : IsNoetherian K V], ↑(IsNoetherian.finsetBasisIndex K V) = Module.Basis.ofVectorSpaceIndex K V
-- Mathlib.Algebra.Group.Basic
add_left_iterate_apply_zero : ∀ {M : Type u_4} [inst : AddMonoid M] {n : ℕ} (a : M), (fun x => a + x)^[n] 0 = n • a
-- Mathlib.Analysis.LocallyConvex.BalancedCoreHull
smul_balancedCore_subset : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : SeminormedRing 𝕜] [inst_1 : SMul 𝕜 E] (s : Set E) {a : 𝕜},
  ‖a‖ ≤ 1 → a • balancedCore 𝕜 s ⊆ balancedCore 𝕜 s
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
/-- A commutative simple group is isomorphic to `ZMod p` from some prime `p`.  -/
exists_prime_addEquiv_ZMod : ∀ {G : Type u_2} [inst : CommGroup G] [IsSimpleGroup G], ∃ p, Nat.Prime p ∧ Nonempty (Additive G ≃+ ZMod p)
-- Mathlib.Computability.NFA
NFA.evalFrom_union : ∀ {α : Type u} {σ : Type v} (M : NFA α σ) (S T : Set σ) (x : List α),
  M.evalFrom (S ∪ T) x = M.evalFrom S x ∪ M.evalFrom T x
-- Mathlib.Analysis.SpecialFunctions.SmoothTransition
expNegInvGlue.eq_1 : ∀ (x : ℝ), expNegInvGlue x = if x ≤ 0 then 0 else Real.exp (-x⁻¹)
-- Mathlib.Topology.Sheaves.Stalks
TopCat.Presheaf.stalkFunctor_map_germ_apply' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C] {X : TopCat}
  {FC : C → C → Type u_1} {CC : C → Type u_2} [inst_2 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)]
  [inst_3 : CategoryTheory.ConcreteCategory C FC] {F G : TopCat.Presheaf C X} (U : TopologicalSpace.Opens ↑X) (x : ↑X)
  (hx : x ∈ U) (f : F ⟶ G) (s : CC (F.obj (Opposite.op U))),
  (CategoryTheory.ConcreteCategory.hom ((TopCat.Presheaf.stalkFunctor C x).map f))
      ((CategoryTheory.ConcreteCategory.hom (F.germ U x hx)) s) =
    (CategoryTheory.ConcreteCategory.hom (G.germ U x hx))
      ((CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op U))) s)
-- Mathlib.Analysis.Normed.Lp.lpSpace
lp.lsingle_apply : ∀ {𝕜 : Type u_1} {α : Type u_3} {E : α → Type u_4} [inst : (i : α) → NormedAddCommGroup (E i)] [inst_1 : NormedRing 𝕜]
  [inst_2 : (i : α) → Module 𝕜 (E i)] [inst_3 : ∀ (i : α), IsBoundedSMul 𝕜 (E i)] [inst_4 : DecidableEq α] (p : ENNReal)
  (i : α) (a : E i), (lp.lsingle p i) a = lp.single p i a
-- Mathlib.RepresentationTheory.Invariants
Representation.invariants_eq_top : ∀ {k : Type u_1} {G : Type u_2} {V : Type u_3} [inst : CommRing k] [inst_1 : Group G] [inst_2 : AddCommGroup V]
  [inst_3 : Module k V] (ρ : Representation k G V) [ρ.IsTrivial], ρ.invariants = ⊤
-- Mathlib.Data.Finset.Sum
Finset.disjSum_mono : ∀ {α : Type u_1} {β : Type u_2} {s₁ s₂ : Finset α} {t₁ t₂ : Finset β}, s₁ ⊆ s₂ → t₁ ⊆ t₂ → s₁.disjSum t₁ ⊆ s₂.disjSum t₂
-- Mathlib.Algebra.Order.GroupWithZero.Basic
antitoneOn_inv_pos : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] [MulPosReflectLT G₀],
  AntitoneOn (fun x => x⁻¹) {r | 0 < r}
-- Mathlib.CategoryTheory.Monad.Limits
/-- The forgetful functor from the Eilenberg-Moore category for a comonad creates any limit
which the comonad itself preserves.
 -/
CategoryTheory.Comonad.forgetCreatesLimit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} J] →
        {T : CategoryTheory.Comonad C} →
          (D : CategoryTheory.Functor J T.Coalgebra) →
            [CategoryTheory.Limits.PreservesLimit (D.comp T.forget) T.toFunctor] →
              [CategoryTheory.Limits.PreservesLimit ((D.comp T.forget).comp T.toFunctor) T.toFunctor] →
                CategoryTheory.CreatesLimit D T.forget
-- Init.Data.List.Attach
List.head?_attachWith : ∀ {α : Type u_1} {P : α → Prop} {xs : List α} (H : ∀ a ∈ xs, P a),
  (xs.attachWith P H).head? = xs.head?.pbind fun a h => some ⟨a, ⋯⟩
-- Init.Data.String.Search
/-- Checks whether a string has a match of the pattern `pat` anywhere.

This function is generic over all currently supported patterns.

Examples:

* `"coffee tea water".contains Char.isWhitespace = true`

* `"tea".contains (fun (c : Char) => c == 'X') = false`

* `"coffee tea water".contains "tea" = true`
 -/
String.contains : {ρ : Type} →
  {σ : String.Slice → Type} →
    [inst : (s : String.Slice) → Std.Iterator (σ s) Id (String.Slice.Pattern.SearchStep s)] →
      [(s : String.Slice) → Std.IteratorLoop (σ s) Id Id] →
        String → (pat : ρ) → [String.Slice.Pattern.ToForwardSearcher pat σ] → Bool
-- Mathlib.Probability.Independence.CharacteristicFunction
/-- Two random variables are independent if and only if their joint characteristic function is equal
to the product of the characteristic functions. This is the version for Banach spaces, see
`indepFun_iff_charFun_prod` for the Hilbert space version.  -/
ProbabilityTheory.indepFun_iff_charFunDual_prod : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {E : Type u_2}
  {F : Type u_3} {mE : MeasurableSpace E} [inst : NormedAddCommGroup E] [BorelSpace E] [SecondCountableTopology E]
  {mF : MeasurableSpace F} [inst_3 : NormedAddCommGroup F] [CompleteSpace F] [BorelSpace F] [SecondCountableTopology F]
  {X : Ω → E} {Y : Ω → F} [inst_7 : NormedSpace ℝ E] [inst_8 : NormedSpace ℝ F] [CompleteSpace E],
  AEMeasurable X P →
    AEMeasurable Y P →
      (ProbabilityTheory.IndepFun X Y P ↔
        ∀ (L : StrongDual ℝ (E × F)),
          MeasureTheory.charFunDual (MeasureTheory.Measure.map (fun ω => (X ω, Y ω)) P) L =
            MeasureTheory.charFunDual (MeasureTheory.Measure.map X P) (L ∘SL ContinuousLinearMap.inl ℝ E F) *
              MeasureTheory.charFunDual (MeasureTheory.Measure.map Y P) (L ∘SL ContinuousLinearMap.inr ℝ E F))
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
tsum_extend_zero : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {γ : Type u_4} {g : γ → β},
  Function.Injective g → ∀ (f : γ → α), ∑' (y : β), Function.extend g f 0 y = ∑' (x : γ), f x
-- Mathlib.RingTheory.Valuation.Basic
Valuation.pos_iff : ∀ {K : Type u_1} [inst : DivisionRing K] {Γ₀ : Type u_4} [inst_1 : LinearOrderedCommMonoidWithZero Γ₀] [Nontrivial Γ₀]
  (v : Valuation K Γ₀) {x : K}, 0 < v x ↔ x ≠ 0
-- Mathlib.Order.Interval.Set.Pi
Set.image_single_Ioc_left : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : DecidableEq ι] [inst_1 : (i : ι) → PartialOrder (α i)]
  [inst_2 : (i : ι) → Zero (α i)] (i : ι) (a : α i), Pi.single i '' Set.Ioc a 0 = Set.Ioc (Pi.single i a) 0
-- Mathlib.Dynamics.BirkhoffSum.NormedSpace
dist_birkhoffSum_birkhoffSum_le : ∀ {α : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] (f : α → α) (g : α → E) (n : ℕ) (x y : α),
  dist (birkhoffSum f g n x) (birkhoffSum f g n y) ≤ ∑ k ∈ Finset.range n, dist (g (f^[k] x)) (g (f^[k] y))
-- Lean.Meta.Tactic.Grind.Arith.Util
Lean.Meta.Grind.Arith.isIntModuleVirtualParent : Option Lean.Expr → Bool
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
ENNReal.rpow_two : ∀ (x : ENNReal), x ^ 2 = x ^ 2
-- Batteries.Recycling.RBTree.Lemmas
_private.Batteries.Recycling.RBTree.Lemmas.0.RBTree.RBNode.Stream.foldl.match_1.eq_1 : ∀ {σ : Sort u_3} {α : Type u_1} (motive : σ → RBTree.RBNode.Stream α → Sort u_2) (b : σ)
  (h_1 : (b : σ) → motive b RBTree.RBNode.Stream.nil)
  (h_2 :
    (b : σ) →
      (v : α) →
        (r : RBTree.RBNode α) → (tail : RBTree.RBNode.Stream α) → motive b (RBTree.RBNode.Stream.cons v r tail)),
  (match b, RBTree.RBNode.Stream.nil with
    | b, RBTree.RBNode.Stream.nil => h_1 b
    | b, RBTree.RBNode.Stream.cons v r tail => h_2 b v r tail) =
    h_1 b
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
/-- The underlying family of 2-morphisms.  -/
CategoryTheory.Oplax.OplaxTrans.Modification.app : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.OplaxFunctor B C} →
          {η θ : F ⟶ G} → CategoryTheory.Oplax.OplaxTrans.Modification η θ → (a : B) → η.app a ⟶ θ.app a
-- Mathlib.Order.Hom.Set
/-- If a function `f` is strictly monotone on a set `s`, then it defines an order isomorphism
between `s` and its image.  -/
StrictMonoOn.orderIso : {α : Type u_4} →
  {β : Type u_5} →
    [inst : LinearOrder α] → [inst_1 : Preorder β] → (f : α → β) → (s : Set α) → StrictMonoOn f s → ↑s ≃o ↑(f '' s)
-- Init.Data.UInt.Bitwise
instAssociativeUInt64HOr : Std.Associative fun x1 x2 => x1 ||| x2
-- Init.Data.SInt.Lemmas
Int32.ofBitVec_mul : ∀ (a b : BitVec 32), Int32.ofBitVec (a * b) = Int32.ofBitVec a * Int32.ofBitVec b
-- Init.Data.Nat.Lcm
Nat.lcm_dvd : ∀ {m n k : ℕ}, m ∣ k → n ∣ k → m.lcm n ∣ k
-- Mathlib.Analysis.Asymptotics.TVS
Asymptotics.IsThetaTVS.trans : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} {G : Type u_6} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommGroup F]
  [inst_5 : TopologicalSpace F] [inst_6 : Module 𝕜 F] [inst_7 : AddCommGroup G] [inst_8 : TopologicalSpace G]
  [inst_9 : Module 𝕜 G] {l : Filter α} {f : α → E} {g : α → F} {k : α → G}, f =Θ[𝕜; l] g → g =Θ[𝕜; l] k → f =Θ[𝕜; l] k
-- Init.Data.Ord.Basic
/-- Compares `a` and `b` lexicographically by `cmp₁` and `cmp₂`.

`a` and `b` are first compared by `cmp₁`. If this returns `Ordering.eq`, `a` and `b` are compared
by `cmp₂` to break the tie.

To lexicographically combine two `Ordering`s, use `Ordering.then`.
 -/
compareLex : {α : Sort u_1} → {β : Sort u_2} → (α → β → Ordering) → (α → β → Ordering) → α → β → Ordering
-- Mathlib.Data.Fin.Fin2
/-- `i + k : Fin2 (n + k)` when `i : Fin2 n` and `k : ℕ`  -/
Fin2.add : {n : ℕ} → Fin2 n → (k : ℕ) → Fin2 (n + k)
-- Batteries.Data.List.Basic
List.swapAtTR.go.eq_2 : ∀ {α : Type u_1} (l : List α) (v : α) (a : Array α) (head : α) (xs : List α),
  List.swapAtTR.go l v (head :: xs) 0 a = (head, a.toListAppend (v :: xs))
-- Mathlib.Topology.Homotopy.HomotopyGroup
GenLoop.currySum_apply_coe : ∀ {N : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {M : Type u_3} (x : X) (q : ↑(GenLoop (M ⊕ N) X x))
  (a : M → ↑unitInterval),
  ↑((GenLoop.currySum x q) a) =
    ((↑q).comp { toFun := Homeomorph.sumArrowHomeomorphProdArrow.invFun, continuous_toFun := ⋯ }).curry.toFun a
-- Mathlib.LinearAlgebra.Dual.Defs
Module.IsReflexive.mk : ∀ {R : Type u_3} {M : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  Function.Bijective ⇑(Module.Dual.eval R M) → Module.IsReflexive R M
-- Mathlib.CategoryTheory.Preadditive.Injective.Basic
/-- Given an equivalence of categories `F`, an injective presentation of `F(X)` induces an
injective presentation of `X.`  -/
CategoryTheory.Equivalence.injectivePresentationOfMapInjectivePresentation : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u_1} →
      [inst_1 : CategoryTheory.Category.{v_1, u_1} D] →
        (F : C ≌ D) →
          (X : C) → CategoryTheory.InjectivePresentation (F.functor.obj X) → CategoryTheory.InjectivePresentation X
-- Mathlib.Algebra.Lie.Basic
LieModuleHom.hasNSMul : {R : Type u} →
  {L : Type v} →
    {M : Type w} →
      {N : Type w₁} →
        [inst : CommRing R] →
          [inst_1 : LieRing L] →
            [inst_2 : AddCommGroup M] →
              [inst_3 : AddCommGroup N] →
                [inst_4 : Module R M] →
                  [inst_5 : Module R N] →
                    [inst_6 : LieRingModule L M] → [inst_7 : LieRingModule L N] → SMul ℕ (M →ₗ⁅R,L⁆ N)
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
/-- The iterated derivative commutes with subtracting a constant.  -/
iteratedFDerivWithin_comp_sub' : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f : E → F} (n : ℕ) (a : E),
  iteratedFDerivWithin 𝕜 n (fun z => f (z - a)) s = fun x => iteratedFDerivWithin 𝕜 n f (-a +ᵥ s) (x - a)
-- Mathlib.Analysis.SpecialFunctions.Complex.Log
/-- **Alias** of `Complex.expOpenPartialHomeomorph`.

---

`Complex.exp` as an `OpenPartialHomeomorph` with `source = {z | -π < im z < π}` and
`target = {z | 0 < re z} ∪ {z | im z ≠ 0}` (a.k.a. `slitPlane`).
This definition is used to prove that `Complex.log`
is complex differentiable at all points but the negative real semi-axis.
 -/
Complex.expPartialHomeomorph : OpenPartialHomeomorph ℂ ℂ
-- Mathlib.GroupTheory.GroupExtension.Defs
/-- The projection homomorphism `E →+ G`  -/
AddGroupExtension.rightHom : {N : Type u_1} →
  {E : Type u_2} →
    {G : Type u_3} →
      [inst : AddGroup N] → [inst_1 : AddGroup E] → [inst_2 : AddGroup G] → AddGroupExtension N E G → E →+ G
-- Mathlib.Data.Int.Cast.Pi
Pi.instIntCast : {ι : Type u_1} → {π : ι → Type u_2} → [(i : ι) → IntCast (π i)] → IntCast ((i : ι) → π i)
-- Std.Sat.AIG.Basic
Std.Sat.AIG.TernaryInput.mk.injEq : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {aig : Std.Sat.AIG α}
  (discr lhs rhs discr_1 lhs_1 rhs_1 : aig.Ref),
  ({ discr := discr, lhs := lhs, rhs := rhs } = { discr := discr_1, lhs := lhs_1, rhs := rhs_1 }) =
    (discr = discr_1 ∧ lhs = lhs_1 ∧ rhs = rhs_1)
-- Mathlib.Topology.IsLocalHomeomorph
/-- A chosen local inverse for a local homeomorphism `f` at a point `x`.  -/
IsLocalHomeomorph.localInverseAt : {X : Type u_1} →
  {Y : Type u_2} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] → {f : X → Y} → IsLocalHomeomorph f → X → OpenPartialHomeomorph Y X
-- Init.Grind.Ring.CommSemiringAdapter
Lean.Grind.CommRing.Expr.toPolyS.eq_def : ∀ (x : Lean.Grind.CommRing.Expr),
  x.toPolyS =
    match x with
    | Lean.Grind.CommRing.Expr.num n => Lean.Grind.CommRing.Poly.num ↑n.natAbs
    | Lean.Grind.CommRing.Expr.var x => Lean.Grind.CommRing.Poly.ofVar x
    | a.add b => a.toPolyS.combine b.toPolyS
    | a.mul b => a.toPolyS.mul b.toPolyS
    | a.pow k =>
      match a with
      | Lean.Grind.CommRing.Expr.num n => Lean.Grind.CommRing.Poly.num (↑n.natAbs ^ k)
      | Lean.Grind.CommRing.Expr.var x =>
        Lean.Grind.CommRing.Poly.ofMon (Lean.Grind.CommRing.Mon.mult { x := x, k := k } Lean.Grind.CommRing.Mon.unit)
      | x => a.toPolyS.pow k
    | Lean.Grind.CommRing.Expr.natCast n => Lean.Grind.CommRing.Poly.num ↑n
    | a.sub b => Lean.Grind.CommRing.Poly.num 0
    | a.neg => Lean.Grind.CommRing.Poly.num 0
    | Lean.Grind.CommRing.Expr.intCast k => Lean.Grind.CommRing.Poly.num 0
-- Mathlib.LinearAlgebra.Dimension.Finite
finrank_eq_zero_of_not_exists_basis_finite : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Module.Free R M],
  (¬∃ s x, s.Finite) → Module.finrank R M = 0
-- Batteries.Data.Stream
Std.Stream.take.eq_def : ∀ {σ : Type u_1} {α : Type u_2} [inst : Std.Stream σ α] (s : σ) (x : ℕ),
  Std.Stream.take s x =
    match x with
    | 0 => ([], s)
    | n.succ =>
      match Std.Stream.next? s with
      | none => ([], s)
      | some (a, s) =>
        match Std.Stream.take s n with
        | (as, s) => (a :: as, s)
-- Init.System.IO
IO.FS.Stream.mk : IO Unit → (USize → IO ByteArray) → (ByteArray → IO Unit) → IO String → (String → IO Unit) → BaseIO Bool → IO.FS.Stream
-- Mathlib.Tactic.Widget.Conv
/-- Return the syntax to insert for the conv widget.
Factored out of `insertEnter` for easy testing.  -/
Mathlib.Tactic.Conv.insertEnterSyntax : Array Lean.SubExpr.GoalsLocation → Lean.Expr → Lean.MetaM Lean.Syntax
-- Mathlib.GroupTheory.HNNExtension
/-- The stable letter of the `HNNExtension`  -/
HNNExtension.t : {G : Type u_1} → [inst : Group G] → {A B : Subgroup G} → {φ : ↥A ≃* ↥B} → HNNExtension G A B φ
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
groupCohomology.cochainsMap_id_f_map_epi : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A B : Rep.{u, u, u} k G} (φ : A ⟶ B) [CategoryTheory.Epi φ]
  (i : ℕ), CategoryTheory.Epi ((groupCohomology.cochainsMap (MonoidHom.id G) φ).f i)
-- Mathlib.Order.CompleteLattice.Defs
/-- A linear order is total.  -/
CompleteLinearOrder.le_total : ∀ {α : Type u_8} [self : CompleteLinearOrder α] (a b : α), a ≤ b ∨ b ≤ a
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
measurableSet_notMem : ∀ {α : Type u_1} (a : α), MeasurableSet {s | a ∉ s}
-- Mathlib.Algebra.Group.Subgroup.Lattice
AddSubgroup.bot_toAddSubmonoid : ∀ {G : Type u_1} [inst : AddGroup G], ⊥.toAddSubmonoid = ⊥
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.isSome_min?_eq_not_isEmpty : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp], t.min?.isSome = !t.isEmpty
-- Batteries.Util.ProofWanted
/-- Parses the surface syntax of `proof_wanted` (a synonym for `theorem_wanted`) and forwards to
the shared `elabWanted`.  -/
elabProofWanted : Lean.Elab.Command.CommandElab
-- Mathlib.AlgebraicTopology.SimplicialNerve
CategoryTheory.SimplicialThickening.id_I : ∀ (J : Type u_1) [inst : LinearOrder J] (i : CategoryTheory.SimplicialThickening J),
  (CategoryTheory.CategoryStruct.id i).I = {i.as}
-- Mathlib.Order.Filter.Germ.Basic
/-- The space of germs of functions `α → β` at a filter `l`.  -/
Filter.Germ : {α : Type u_1} → Filter α → Type u_5 → Type (max u_1 u_5)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Complex.iteratedDeriv_add_one_sinh : ∀ (n : ℕ), iteratedDeriv (n + 1) Complex.sinh = iteratedDeriv n Complex.cosh
-- Mathlib.CategoryTheory.Adjunction.FullyFaithful
/-- If the counit of an adjunction is an isomorphism, then its inverse on the image of R is given
by R whiskered with the unit.  -/
CategoryTheory.Adjunction.inv_counit_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) {X : D}
  [inst_2 : CategoryTheory.IsIso (h.counit.app X)], CategoryTheory.inv (R.map (h.counit.app X)) = h.unit.app (R.obj X)
-- Mathlib.Analysis.Normed.Group.InfiniteSum
Summable.of_enorm : ∀ {ι : Type u_1} {E : Type u_3} [inst : SeminormedAddCommGroup E] [CompleteSpace E] {f : ι → E},
  ∑' (a : ι), ‖f a‖ₑ ≠ ⊤ → Summable f
-- Mathlib.Order.Bounds.Image
bddAbove_pi : ∀ {α : Type u} {π : α → Type u_1} [inst : (a : α) → Preorder (π a)] {s : Set ((a : α) → π a)},
  BddAbove s ↔ ∀ (a : α), BddAbove (Function.eval a '' s)
-- Mathlib.NumberTheory.NumberField.Completion.FinitePlace
NumberField.FinitePlace.apply_mul_absNorm_pow_eq_one : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] (v : NumberField.FinitePlace K)
  {x : NumberField.RingOfIntegers K},
  x ≠ 0 → v ↑x * ↑(Ideal.absNorm v.maximalIdeal.asIdeal) ^ multiplicity v.maximalIdeal.asIdeal (Ideal.span {x}) = 1
-- Mathlib.ModelTheory.Order
/-- A sentence indicating that an order has no top element:
$\forall x, \exists y, \neg y \le x$.  -/
FirstOrder.Language.noTopOrderSentence : (L : FirstOrder.Language) → [L.IsOrdered] → L.Sentence
-- Mathlib.LinearAlgebra.Finsupp.VectorSpace
Finsupp.linearIndependent_single : ∀ {R : Type u_1} {M : Type u_2} {ι : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {φ : ι → Type u_4} (f : (i : ι) → φ i → M),
  (∀ (i : ι), LinearIndependent R (f i)) → LinearIndependent R fun ix => fun₀ | ix.fst => f ix.fst ix.snd
-- Lean.Data.Lsp.Extra
Lean.Lsp.instToJsonHighlightMatchesOptions : Lean.ToJson Lean.Lsp.HighlightMatchesOptions
-- Mathlib.Algebra.Group.NatPowAssoc
Monoid.PowAssoc : ∀ {M : Type u_1} [inst : Monoid M], NatPowAssoc M
-- Mathlib.Algebra.Regular.Opposite
isAddRegular_op : ∀ {R : Type u_1} [inst : Add R] {a : R}, IsAddRegular (AddOpposite.op a) ↔ IsAddRegular a
-- Std.Data.Internal.List.Associative
Std.Internal.List.replaceEntry_cons_of_true : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {l : List ((a : α) × β a)} {k k' : α} {v : β k} {v' : β k'},
  (k' == k) = true → Std.Internal.List.replaceEntry k v (⟨k', v'⟩ :: l) = ⟨k, v⟩ :: l
-- Init.Data.Iterators.Basic
/-- `Rel` is well-founded.  -/
Std.Iterators.FinitenessRelation.wf : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} [inst : Std.Iterator α m β]
  (self : Std.Iterators.FinitenessRelation α m), WellFounded self.Rel
-- Init.Data.String.Basic
String.utf8ByteSize_singleton : ∀ {c : Char}, (String.singleton c).utf8ByteSize = c.utf8Size
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
extChartAt_source_mem_nhds : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  {I : ModelWithCorners 𝕜 E H} [inst_5 : ChartedSpace H M] (x : M), (extChartAt I x).source ∈ nhds x
-- Mathlib.MeasureTheory.PiSystem
isPiSystem_Ioc_mem : ∀ {α : Type u_1} [inst : LinearOrder α] (s t : Set α), IsPiSystem {S | ∃ l ∈ s, ∃ u ∈ t, l < u ∧ Set.Ioc l u = S}
-- Mathlib.Algebra.Order.Floor.Ring
Int.fract_eq_fract : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] [IsOrderedRing R] {a b : R},
  Int.fract a = Int.fract b ↔ ∃ z, a - b = ↑z
-- Mathlib.Data.NNReal.Defs
NNReal.canLift : CanLift ℝ NNReal NNReal.toReal fun r => 0 ≤ r