mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Category.TopCat.Limits.Products
TopCat.piIsoPi_inv_π : ∀ {ι : Type v} (α : ι → TopCat) (i : ι),
  CategoryTheory.CategoryStruct.comp (TopCat.piIsoPi α).inv (CategoryTheory.Limits.Pi.π α i) = TopCat.piπ α i
-- Mathlib.Algebra.Polynomial.Degree.Support
Polynomial.supp_subset_range : ∀ {R : Type u} {m : ℕ} [inst : Semiring R] {p : Polynomial R}, p.natDegree < m → p.support ⊆ Finset.range m
-- Mathlib.CategoryTheory.Extensive
CategoryTheory.finitaryExtensive_iff_of_isTerminal : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasFiniteCoproducts C]
  [CategoryTheory.HasPullbacksOfInclusions C] (T : C) (HT : CategoryTheory.Limits.IsTerminal T)
  (c₀ : CategoryTheory.Limits.BinaryCofan T T) (hc₀ : CategoryTheory.Limits.IsColimit c₀),
  CategoryTheory.FinitaryExtensive C ↔ CategoryTheory.IsVanKampenColimit c₀
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.rightUnitor_naturality : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : B} {f g : a ⟶ b} (η : f ⟶ g),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight η (CategoryTheory.CategoryStruct.id b))
      (CategoryTheory.Bicategory.rightUnitor g).hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor f).hom η
-- Mathlib.Data.Set.Card
Set.ncard_insert_of_mem : ∀ {α : Type u_1} {s : Set α} {a : α}, a ∈ s → (insert a s).ncard = s.ncard
-- Std.Sat.AIG.Lemmas
Std.Sat.AIG.Ref.cast.congr_simp : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {aig1 aig2 : Std.Sat.AIG α} (ref ref_1 : aig1.Ref),
  ref = ref_1 → ∀ (h : aig1.decls.size ≤ aig2.decls.size), ref.cast h = ref_1.cast h
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.find?_toList_eq_none_iff_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {k : α},
      List.find? (fun x => cmp x.1 k == Ordering.eq) (Std.DTreeMap.Raw.Const.toList t) = none ↔ t.contains k = false
-- Mathlib.Algebra.Homology.Factorizations.CM5b
/-- The second projection `p K L : mappingCone (𝟙 (I K)) ⊞ L ⟶ L` is a homotopy equivalence.  -/
CochainComplex.cm5b.homotopyEquiv : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      [inst_2 : CategoryTheory.EnoughInjectives C] →
        (K L : CochainComplex C ℤ) →
          HomotopyEquiv (CochainComplex.mappingCone (CategoryTheory.CategoryStruct.id (CochainComplex.cm5b.I K)) ⊞ L) L
-- Mathlib.GroupTheory.Finiteness
AddMonoid.multiples_fg : ∀ {M : Type u_1} [inst : AddMonoid M] (r : M), AddMonoid.FG ↥(AddSubmonoid.multiples r)
-- Mathlib.Algebra.Lie.TraceForm
killingForm_eq_zero_of_mem_zeroRoot_mem_posFitting : ∀ (R : Type u_1) (L : Type u_3) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  (H : LieSubalgebra R L) [inst_3 : LieRing.IsNilpotent ↥H] {x₀ x₁ : L},
  x₀ ∈ LieAlgebra.zeroRootSubalgebra R L H → x₁ ∈ LieModule.posFittingComp R (↥H) L → ((killingForm R L) x₀) x₁ = 0
-- Mathlib.Data.Set.Function
Set.imageFactorization.eq_1 : ∀ {α : Type u} {β : Type v} (f : α → β) (s : Set α) (p : ↑s), Set.imageFactorization f s p = ⟨f ↑p, ⋯⟩
-- Mathlib.Data.Vector.Basic
/-- `set v n a` replaces the `n`th element of `v` with `a`.  -/
List.Vector.set : {α : Type u_1} → {n : ℕ} → List.Vector α n → Fin n → α → List.Vector α n
-- Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
/-- Any maximally `Kᵣ₊₂`-free graph that is not complete-multipartite contains a maximal
`IsFiveWheelLike` structure `Wᵣ,ₖ` for some `k < r`. (It is maximal in terms of `k`.)
 -/
SimpleGraph.exists_max_isFiveWheelLike_of_maximal_cliqueFree_not_isCompleteMultipartite : ∀ {α : Type u_1} {G : SimpleGraph α} {r : ℕ} [inst : DecidableEq α],
  Maximal (fun H => H.CliqueFree (r + 2)) G →
    ¬G.IsCompleteMultipartite →
      ∃ k v w₁ w₂ s t, G.IsFiveWheelLike r k v w₁ w₂ s t ∧ k < r ∧ ∀ (j : ℕ), k < j → G.FiveWheelLikeFree r j
-- Mathlib.Algebra.Order.Interval.Set.Group
Set.pairwise_disjoint_Ico_add_zsmul : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] (a b : α),
  Pairwise (Function.onFun Disjoint fun n => Set.Ico (a + n • b) (a + (n + 1) • b))
-- Mathlib.Analysis.Real.OfDigits
/-- A generalization of the identity `0.(9) = 1` to arbitrary positional numeral systems.  -/
Real.ofDigits_const_last_eq_one' : ∀ {b : ℕ} (hb : 1 < b), (Real.ofDigits fun x => ⟨b - 1, ⋯⟩) = 1
-- Mathlib.Data.Multiset.ZeroCons
Multiset.exists_mem_of_ne_zero : ∀ {α : Type u_1} {s : Multiset α}, s ≠ 0 → ∃ a, a ∈ s
-- Mathlib.Algebra.Order.Group.Synonym
Colex.instAddLeftCancelMonoid : {α : Type u_1} → [AddLeftCancelMonoid α] → AddLeftCancelMonoid (Colex α)
-- Init.Data.Int.DivMod.Lemmas
Int.mul_tdiv_cancel' : ∀ {a b : ℤ}, a ∣ b → a * b.tdiv a = b
-- Mathlib.Topology.MetricSpace.Algebra
/-- The typeclass `IsBoundedSMul` on a metric-space scalar action implies continuity of the
action.  -/
IsBoundedSMul.continuousSMul : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] [inst_2 : Zero α]
  [inst_3 : Zero β] [inst_4 : SMul α β] [IsBoundedSMul α β], ContinuousSMul α β
-- Mathlib.FieldTheory.Minpoly.Field
/-- If an element `x` is a root of a polynomial `p`, then the minimal polynomial of `x` divides `p`.
See also `minpoly.isIntegrallyClosed_dvd` which relaxes the assumptions on `A` in exchange for
stronger assumptions on `B`.  -/
minpoly.dvd : ∀ (A : Type u_1) {B : Type u_2} [inst : Field A] [inst_1 : Ring B] [inst_2 : Algebra A B] (x : B) {p : Polynomial A},
  (Polynomial.aeval x) p = 0 → minpoly A x ∣ p
-- Batteries.Recycling.RBTree.Basic
_private.Batteries.Recycling.RBTree.Basic.0.RBTree.RBNode.append.match_1.eq_5 : ∀ {α : Type u_1} (motive : RBTree.RBNode α → RBTree.RBNode α → Sort u_2) (l : RBTree.RBNode α) (v : α)
  (r b : RBTree.RBNode α) (x : α) (c : RBTree.RBNode α) (h_1 : (x : RBTree.RBNode α) → motive RBTree.RBNode.nil x)
  (h_2 : (x : RBTree.RBNode α) → motive x RBTree.RBNode.nil)
  (h_3 :
    (a : RBTree.RBNode α) →
      (x : α) →
        (b c : RBTree.RBNode α) →
          (y : α) →
            (d : RBTree.RBNode α) →
              motive (RBTree.RBNode.node RBTree.RBColor.red a x b) (RBTree.RBNode.node RBTree.RBColor.red c y d))
  (h_4 :
    (a : RBTree.RBNode α) →
      (x : α) →
        (b c : RBTree.RBNode α) →
          (y : α) →
            (d : RBTree.RBNode α) →
              motive (RBTree.RBNode.node RBTree.RBColor.black a x b) (RBTree.RBNode.node RBTree.RBColor.black c y d))
  (h_5 :
    (a l : RBTree.RBNode α) →
      (v : α) →
        (r : RBTree.RBNode α) →
          a = RBTree.RBNode.node RBTree.RBColor.black l v r →
            (b : RBTree.RBNode α) →
              (x : α) →
                (c : RBTree.RBNode α) →
                  motive (RBTree.RBNode.node RBTree.RBColor.black l v r) (RBTree.RBNode.node RBTree.RBColor.red b x c))
  (h_6 :
    (a : RBTree.RBNode α) →
      (x : α) →
        (b c l : RBTree.RBNode α) →
          (v : α) →
            (r : RBTree.RBNode α) →
              c = RBTree.RBNode.node RBTree.RBColor.black l v r →
                motive (RBTree.RBNode.node RBTree.RBColor.red a x b) (RBTree.RBNode.node RBTree.RBColor.black l v r)),
  (match RBTree.RBNode.node RBTree.RBColor.black l v r, RBTree.RBNode.node RBTree.RBColor.red b x c with
    | RBTree.RBNode.nil, x => h_1 x
    | x, RBTree.RBNode.nil => h_2 x
    | RBTree.RBNode.node RBTree.RBColor.red a x b, RBTree.RBNode.node RBTree.RBColor.red c y d => h_3 a x b c y d
    | RBTree.RBNode.node RBTree.RBColor.black a x b, RBTree.RBNode.node RBTree.RBColor.black c y d => h_4 a x b c y d
    | a@h:(RBTree.RBNode.node RBTree.RBColor.black l v r), RBTree.RBNode.node RBTree.RBColor.red b x c =>
      h_5 a l v r h b x c
    | RBTree.RBNode.node RBTree.RBColor.red a x b, c@h:(RBTree.RBNode.node RBTree.RBColor.black l v r) =>
      h_6 a x b c l v r h) =
    h_5 (RBTree.RBNode.node RBTree.RBColor.black l v r) l v r ⋯ b x c
-- Mathlib.Analysis.Analytic.Basic
/-- If a function admits a power series expansion within a set at `x`, then it is the locally
uniform limit of the partial sums of this power series on the disk of convergence, i.e., `f y`
is the locally uniform limit of `p.partialSum n (y - x)` there.  -/
HasFPowerSeriesWithinOnBall.tendstoLocallyUniformlyOn' : ∀ {𝕜 : 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] {f : E → F}
  {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E} {r : ENNReal},
  HasFPowerSeriesWithinOnBall f p s x r →
    TendstoLocallyUniformlyOn (fun n y => p.partialSum n (y - x)) f Filter.atTop (insert x s ∩ Metric.eball x r)
-- Mathlib.Topology.MetricSpace.Thickening
/-- The closed thickening of a set contains the closure of the set.  -/
Metric.closure_subset_cthickening : ∀ {α : Type u} [inst : PseudoEMetricSpace α] (δ : ℝ) (E : Set α), closure E ⊆ Metric.cthickening δ E
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Maps
HomogeneousIdeal.toIdeal_map : ∀ {A : Type u_1} {B : Type u_2} {σ : Type u_4} {τ : Type u_5} {ι : Type u_7} [inst : Semiring A] [inst_1 : Semiring B]
  [inst_2 : SetLike σ A] [inst_3 : SetLike τ B] [inst_4 : AddSubmonoidClass σ A] [inst_5 : AddSubmonoidClass τ B]
  [inst_6 : DecidableEq ι] [inst_7 : AddMonoid ι] {𝒜 : ι → σ} {ℬ : ι → τ} [inst_8 : GradedRing 𝒜]
  [inst_9 : GradedRing ℬ] (f : 𝒜 →+*ᵍ ℬ) {I : HomogeneousIdeal 𝒜},
  (HomogeneousIdeal.map f I).toIdeal = Ideal.map f I.toIdeal
-- Mathlib.Order.InitialSeg
InitialSeg.mk.sizeOf_spec : ∀ {α : Type u_4} {β : Type u_5} {r : α → α → Prop} {s : β → β → Prop} [inst : SizeOf α] [inst_1 : SizeOf β]
  [inst_2 : (a a_1 : α) → SizeOf (r a a_1)] [inst_3 : (a a_1 : β) → SizeOf (s a a_1)] (toRelEmbedding : r ↪r s)
  (mem_range_of_rel' : ∀ (a : α) (b : β), s b (toRelEmbedding a) → b ∈ Set.range ⇑toRelEmbedding),
  sizeOf { toRelEmbedding := toRelEmbedding, mem_range_of_rel' := mem_range_of_rel' } = 1 + sizeOf toRelEmbedding
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw.fold_eq_foldl_toListModel : ∀ {α : Type u} {β : α → Type v} {γ : Type w} {l : Std.DHashMap.Raw α β} {f : γ → (a : α) → β a → γ} {init : γ},
  Std.DHashMap.Raw.fold f init l =
    List.foldl (fun a b => f a b.fst b.snd) init (Std.DHashMap.Internal.toListModel l.buckets)
-- Lean.Parser.Syntax
Lean.Parser.syntaxParser : optParam ℕ 0 → Lean.Parser.Parser
-- Init.Data.Option.Monadic
Option.forIn_none : ∀ {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} [inst : Monad m] (b : β) (f : α → β → m (ForInStep β)),
  forIn none b f = pure b
-- Mathlib.Data.Vector.MapLemmas
List.Vector.map_pmap : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {n : ℕ} (xs : List.Vector α n) {p : α → Prop} (f₁ : β → γ)
  (f₂ : (a : α) → p a → β) (H : ∀ x ∈ xs.toList, p x),
  List.Vector.map f₁ (List.Vector.pmap f₂ xs H) = List.Vector.pmap (fun x hx => f₁ (f₂ x hx)) xs H
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.Const.entryAtIdx?.match_1.eq_2 : ∀ {α : Type u_1} {β : Type u_2} (motive : (Std.DTreeMap.Internal.Impl α fun x => β) → ℕ → Sort u_3) (size : ℕ) (k : α)
  (v : β) (l r : Std.DTreeMap.Internal.Impl α fun x => β) (n : ℕ)
  (h_1 : (x : ℕ) → motive Std.DTreeMap.Internal.Impl.leaf x)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β) →
          (l r : Std.DTreeMap.Internal.Impl α fun x => β) →
            (n : ℕ) → motive (Std.DTreeMap.Internal.Impl.inner size k v l r) n),
  (match Std.DTreeMap.Internal.Impl.inner size k v l r, n with
    | Std.DTreeMap.Internal.Impl.leaf, x => h_1 x
    | Std.DTreeMap.Internal.Impl.inner size k v l r, n => h_2 size k v l r n) =
    h_2 size k v l r n
-- Lean.Parser.Level
Lean.Parser.Level.num : Lean.Parser.Parser
-- Mathlib.Data.Int.Log
/-- Over suitable subtypes, `zpow` and `Int.log` form a Galois coinsertion  -/
Int.zpowLogGi : (R : Type u_1) →
  [inst : Semifield R] →
    [inst_1 : LinearOrder R] →
      [inst_2 : IsStrictOrderedRing R] →
        [inst_3 : FloorSemiring R] →
          {b : ℕ} → (hb : 1 < b) → GaloisCoinsertion (fun z => ⟨↑b ^ z, ⋯⟩) fun r => Int.log b ↑r
-- Mathlib.RingTheory.WittVector.Basic
_private.Mathlib.RingTheory.WittVector.Basic.0.WittVector.comm_ring_aux₁ : (p : ℕ) → (R : Type u_1) → [Fact (Nat.Prime p)] → CommRing (WittVector p (MvPolynomial R ℚ))
-- Init.Data.Rat.Lemmas
Rat.mkRat_def : ∀ (n : ℤ) (d : ℕ), mkRat n d = if d0 : d = 0 then 0 else Rat.normalize n d d0
-- Mathlib.Data.Finset.SMulAntidiagonal
/-- `Finset.SMulAntidiagonal hs ht a` is the set of all pairs of an element in `s` and an
element in `t` whose scalar multiplication yields `a`, but its construction requires a proof that
the set-theoretic antidiagonal is finite.  -/
Finset.SMulAntidiagonal : {G : Type u_1} →
  {P : Type u_2} →
    [inst : SMul G P] → {s : Set G} → {t : Set P} → (a : P) → (s.smulAntidiagonal t a).Finite → Finset (G × P)
-- Aesop.Util.UnorderedArraySet
Aesop.UnorderedArraySet.toArray : {α : Type u_1} → [inst : BEq α] → Aesop.UnorderedArraySet α → Array α
-- Mathlib.Topology.MetricSpace.Defs
MetricSpace.eq_of_dist_eq_zero : ∀ {α : Type u} [self : MetricSpace α] {x y : α}, dist x y = 0 → x = y
-- Mathlib.Analysis.LocallyConvex.WithSeminorms
/-- If a family of seminorms is continuous, then their basis sets are neighborhoods of zero.  -/
SeminormFamily.basisSets_mem_nhds : ∀ {𝕜 : Type u_11} {E : Type u_12} {ι : Type u_13} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] (p : SeminormFamily 𝕜 E ι),
  (∀ (i : ι), Continuous ⇑(p i)) → ∀ U ∈ p.basisSets, U ∈ nhds 0
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.Word.fstIdx_cons : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] {i : ι} (m : M i) (w : Monoid.CoprodI.Word M)
  (hmw : w.fstIdx ≠ some i) (h1 : m ≠ 1), (Monoid.CoprodI.Word.cons m w hmw h1).fstIdx = some i
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.getStarResult : {α : Type} →
  Std.HashMap Lean.Meta.LazyDiscrTree.Key Lean.Meta.LazyDiscrTree.TrieIndex →
    Lean.Meta.LazyDiscrTree.MatchM α (Lean.Meta.LazyDiscrTree.MatchResult α)
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.LeftHomologyData.ofEpiOfIsIsoOfMono'_H : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (h : S₂.LeftHomologyData) [inst_2 : CategoryTheory.Epi φ.τ₁]
  [inst_3 : CategoryTheory.IsIso φ.τ₂] [inst_4 : CategoryTheory.Mono φ.τ₃],
  (CategoryTheory.ShortComplex.LeftHomologyData.ofEpiOfIsIsoOfMono' φ h).H = h.H
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.get_min? : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [inst : Std.TransCmp cmp] (h : t.WF) {km : α}
  {hc : t.contains km = true}, t.min?.get ⋯ = km → t.get km hc = km
-- Mathlib.Algebra.Ring.Subring.Defs
Subring.instPartialOrder : {R : Type u} → [inst : NonAssocRing R] → PartialOrder (Subring R)
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Const.RocSliceData.mk : {α : Type u} →
  {β : Type v} →
    [inst : Ord α] →
      (Std.DTreeMap.Internal.Impl α fun x => β) → Std.Roc α → Std.DTreeMap.Internal.Const.RocSliceData α β
-- Mathlib.Topology.VectorBundle.Basic
VectorBundleCore.continuousOn_coordChange : ∀ {R : Type u_1} {B : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField R] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace R F] [inst_3 : TopologicalSpace B] {ι : Type u_5} (self : VectorBundleCore R B F ι) (i j : ι),
  ContinuousOn (self.coordChange i j) (self.baseSet i ∩ self.baseSet j)
-- Mathlib.Topology.Category.TopCat.Opens
TopologicalSpace.Opens.inclusion'_map_eq_top : ∀ {X : TopCat} (U : TopologicalSpace.Opens ↑X), (TopologicalSpace.Opens.map U.inclusion').obj U = ⊤
-- Mathlib.Tactic.GCongr.Core
/-- If `e` is of the form `r a b`, return `(r, a, b)`.
Note: we assume that `e` does not have an `Expr.mdata` annotation.  -/
Mathlib.Tactic.GCongr.getRel : Lean.Expr → Option (Lean.Name × Lean.Expr × Lean.Expr)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.contains_maxKey! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Inhabited α], t.WF → t.isEmpty = false → Std.DTreeMap.Internal.Impl.contains t.maxKey! t = true
-- Init.Data.UInt.Bitwise
UInt64.ofFin_shiftRight : ∀ (a b : Fin UInt64.size), ↑b < 64 → UInt64.ofFin (a >>> b) = UInt64.ofFin a >>> UInt64.ofFin b
-- Mathlib.Condensed.TopCatAdjunction
/-- `simp`-normal form of the lemma that `@[simps]` would generate.  -/
CondensedSet.topCatAdjunctionCounit_hom_apply : ∀ (X : TopCat) (x : C(PUnit.{u_1 + 1}, ↑X)), (TopCat.Hom.hom (CondensedSet.topCatAdjunctionCounit X)) x = x PUnit.unit
-- Mathlib.Data.Set.Lattice.Image
Set.seq_seq : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set (β → γ)} {t : Set (α → β)} {u : Set α},
  s.seq (t.seq u) = (((fun x1 x2 => x1 ∘ x2) '' s).seq t).seq u
-- Init.Grind.Config
/-- When `true` (default: `true`), enables the procedure for handling injective functions.
In this mode, `grind` takes into account theorems such as:
```
@[grind inj] theorem double_inj : Function.Injective double
```
 -/
Lean.Grind.Config.inj : Lean.Grind.Config → Bool
-- Mathlib.GroupTheory.OrderOfElement
addOrderOf_ne_zero_iff : ∀ {G : Type u_1} [inst : AddMonoid G] {x : G}, addOrderOf x ≠ 0 ↔ IsOfFinAddOrder x
-- Mathlib.RingTheory.Polynomial.Resultant.Basic
/-- `Res(f, X - r) = (-1)^{deg f} * f(r)`  -/
Polynomial.resultant_X_sub_C_right : ∀ {R : Type u_1} [inst : CommRing R] (f : Polynomial R) (m : ℕ) (r : R),
  f.natDegree ≤ m → f.resultant (Polynomial.X - Polynomial.C r) m 1 = (-1) ^ m * Polynomial.eval r f
-- Mathlib.LinearAlgebra.LinearIndependent.Lemmas
LinearIndepOn.linearIndepOn_extend : ∀ {ι : Type u'} {K : Type u_3} {V : Type u} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  {v : ι → V} {s t : Set ι} (hs : LinearIndepOn K v s) (hst : s ⊆ t), LinearIndepOn K v (hs.extend hst)
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValue?.eq_1 : ∀ {α : Type u} {β : Type v} [inst : BEq α] (a : α), Std.Internal.List.getValue? a [] = none
-- Lean.Meta.Tactic.Grind.Types
/-- Returns `some n` if `e` has already been "internalized" into the
Otherwise, returns `none`s.
 -/
Lean.Meta.Grind.getENode? : Lean.Expr → Lean.Meta.Grind.GoalM (Option Lean.Meta.Grind.ENode)
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.invertibleEquivInvertibleFst_apply_invOf : ∀ {R : Type u} {M : Type v} [inst : AddCommGroup M] [inst_1 : Semiring R] [inst_2 : Module Rᵐᵒᵖ M] [inst_3 : Module R M]
  [inst_4 : SMulCommClass R Rᵐᵒᵖ M] (x : TrivSqZeroExt R M) (x_1 : Invertible x), ⅟x.fst = (⅟x).fst
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKeyD_insert_self : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], (↑m).WF → ∀ {a fallback : α} {b : β a}, (m.insert a b).getKeyD a fallback = a
-- Mathlib.RingTheory.Regular.Category
ModuleCat.smulShortComplex_exact : ∀ {R : Type u} [inst : CommRing R] (M : ModuleCat R) (r : R), (M.smulShortComplex r).Exact
-- Mathlib.Algebra.Order.Group.Synonym
OrderDual.instSemigroup.eq_1 : ∀ {α : Type u_1} [inst : Semigroup α], OrderDual.instSemigroup = { toMul := OrderDual.instMul, mul_assoc := ⋯ }
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
cfcₙHom_eq_cfcₙ_extend : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : Nontrivial R] [inst_2 : StarRing R]
  [inst_3 : MetricSpace R] [inst_4 : IsTopologicalSemiring R] [inst_5 : ContinuousStar R] [inst_6 : NonUnitalRing A]
  [inst_7 : StarRing A] [inst_8 : TopologicalSpace A] [inst_9 : Module R A] [inst_10 : IsScalarTower R A A]
  [inst_11 : SMulCommClass R A A] [instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p] {a : A} (g : R → R)
  (ha : p a) (f : ContinuousMapZero (↑(quasispectrum R a)) R),
  (cfcₙHom ha) f = cfcₙ (Function.extend Subtype.val (⇑f) g) a
-- Lean.Server.References
/-- Name of the module that this ilean data has been collected for.  -/
Lean.Server.Ilean.module : Lean.Server.Ilean → Lean.Name
-- Init.Data.Iterators.Consumers.Monadic.Loop
/-- Steps through the whole iterator, counting the number of outputs emitted.

**Performance**:

This function's runtime is linear in the number of steps taken by the iterator.
 -/
Std.IterM.Partial.count : {α : Type w} →
  {m : Type w → Type w'} →
    {β : Type w} →
      [inst : Std.Iterator α m β] → [Std.IteratorLoop α m m] → [Monad m] → Std.IterM.Partial m β → m (ULift.{w, 0} ℕ)
-- Mathlib.NumberTheory.LSeries.AbstractFuncEq
/-- Reformulated functional equation with `f` and `g` interchanged.  -/
WeakFEPair.h_feq' : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (P : WeakFEPair E) (x : ℝ),
  0 < x → P.g (1 / x) = (P.ε⁻¹ * ↑(x ^ P.k)) • P.f x
-- Mathlib.LinearAlgebra.UnitaryGroup
Matrix.UnitaryGroup.coeMatrix : {n : Type u} →
  [inst : DecidableEq n] →
    [inst_1 : Fintype n] →
      {α : Type v} → [inst_2 : CommRing α] → [inst_3 : StarRing α] → Coe (↥(Matrix.unitaryGroup n α)) (Matrix n n α)
-- Mathlib.Combinatorics.Hypergraph.Basic
Hypergraph.image_edgeSet : ∀ {α : Type u_1} {β : Type u_2} (H : Hypergraph α) (f : α → β), (H.image f).edgeSet = Set.image f '' H.edgeSet
-- Mathlib.Data.TypeVec
TypeVec.diagSub.eq_def : ∀ {n : ℕ} {α : TypeVec.{u} n} (x : Fin2 n) (x_1 : α x),
  TypeVec.diagSub x x_1 =
    match n, α, x, x_1 with
    | .(n + 1), α, a.fs, x => TypeVec.diagSub a x
    | .(n + 1), α, Fin2.fz, x => ⟨(x, x), ⋯⟩
-- Mathlib.Algebra.FreeMonoid.Count
FreeMonoid.count_of : ∀ {α : Type u_1} [inst : DecidableEq α] (x y : α),
  (FreeMonoid.count x) (FreeMonoid.of y) = Pi.mulSingle x (Multiplicative.ofAdd 1) y
-- Mathlib.CategoryTheory.Yoneda
/-- Representing `F` composed with universe lifting is the same as representing `F`.  -/
CategoryTheory.Functor.representableByUliftFunctorEquiv : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {F : CategoryTheory.Functor Cᵒᵖ (Type v)} →
      {X : C} → (F.comp CategoryTheory.uliftFunctor.{w, v}).RepresentableBy X ≃ F.RepresentableBy X
-- Mathlib.Analysis.Normed.Operator.CompleteCodomain
/-- If a space of linear maps from `E` to `F` is complete, and `E` is nontrivial, then `F` is
complete.  -/
SeparatingDual.completeSpace_of_completeSpace_continuousLinearMap : ∀ (𝕜 : 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] [SeparatingDual 𝕜 E]
  [Nontrivial E] [CompleteSpace (E →L[𝕜] F)], CompleteSpace F
-- Mathlib.Order.Interval.Finset.Fin
Fin.finsetImage_castAdd_Ioo : ∀ {n : ℕ} (m : ℕ) (i j : Fin n),
  Finset.image (Fin.castAdd m) (Finset.Ioo i j) = Finset.Ioo (Fin.castAdd m i) (Fin.castAdd m j)
-- Mathlib.Geometry.Manifold.Riemannian.Basic
IsRiemannianManifold.mk : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type u_2} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type u_3} [inst_3 : TopologicalSpace M] [inst_4 : PseudoEMetricSpace M]
  [inst_5 : ChartedSpace H M] [inst_6 : Bundle.RiemannianBundle fun x => TangentSpace I x],
  (∀ (x y : M), edist x y = Manifold.riemannianEDist I x y) → IsRiemannianManifold I M
-- Mathlib.Algebra.Polynomial.UnitTrinomial
Polynomial.isUnitTrinomial_iff'' : ∀ {p q : Polynomial ℤ}, p * p.mirror = q * q.mirror → (p.IsUnitTrinomial ↔ q.IsUnitTrinomial)
-- Init.Data.String.Lemmas.IsEmpty
String.Slice.isEmpty_slice_eq_false_iff : ∀ {s : String.Slice} {p₁ p₂ : s.Pos} {h : p₁ ≤ p₂}, (s.slice p₁ p₂ h).isEmpty = false ↔ p₁ ≠ p₂
-- Mathlib.RingTheory.Ideal.Maps
/-- **Alias** of the reverse direction of `Ideal.isMaximal_comap_iff_of_bijective`. -/
Ideal.IsMaximal.comap_bijective : ∀ {R : Type u} {S : Type v} {F : Type u_1} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : FunLike F R S] (f : F)
  [inst_3 : RingHomClass F R S], Function.Bijective ⇑f → ∀ {K : Ideal S}, K.IsMaximal → (Ideal.comap f K).IsMaximal
-- Std.Http.Protocol.H1.Reader
/-- Parse body bytes until EOF (connection close).
 -/
Std.Http.Protocol.H1.Reader.BodyState.closeDelimited : Std.Http.Protocol.H1.Reader.BodyState