mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.π_descTruncGE_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} 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]
  (t : CategoryTheory.Triangulated.TStructure C) {X Y : C} (f : X ⟶ Y) (n : ℤ) [inst_6 : t.IsGE Y n] {Z : C}
  (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((t.truncGEπ n).app X) (CategoryTheory.CategoryStruct.comp (t.descTruncGE f n) h) =
    CategoryTheory.CategoryStruct.comp f h
-- Mathlib.Topology.Separation.Hausdorff
isOpen_ne_fun : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [T2Space X] {f g : Y → X},
  Continuous f → Continuous g → IsOpen {y | f y ≠ g y}
-- Aesop.Percent
Aesop.Percent.instHPowNat : HPow Aesop.Percent ℕ Aesop.Percent
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithTop.natCast_ne_top : ∀ {α : Type u} [inst : AddMonoidWithOne α] (n : ℕ), ↑n ≠ ⊤
-- Mathlib.AlgebraicTopology.DoldKan.NCompGamma
/-- The natural transformation `N₁ ⋙ Γ₂ ⟶ toKaroubi (SimplicialObject C)`.  -/
AlgebraicTopology.DoldKan.Γ₂N₁.natTrans : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasFiniteCoproducts C] →
        AlgebraicTopology.DoldKan.N₁.comp AlgebraicTopology.DoldKan.Γ₂ ⟶
          CategoryTheory.Idempotents.toKaroubi (CategoryTheory.SimplicialObject C)
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.getKey!_union_of_not_mem_right : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [inst : Inhabited α] [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α}, k ∉ t₂ → (t₁ ∪ t₂).get! k = t₁.get! k
-- Mathlib.Algebra.Polynomial.Coeff
/-- Decomposes the coefficient of the product `p * q` as a sum
over `antidiagonal`. A version which sums over `range (n + 1)` can be obtained
by using `Finset.Nat.sum_antidiagonal_eq_sum_range_succ`.  -/
Polynomial.coeff_mul : ∀ {R : Type u} [inst : Semiring R] (p q : Polynomial R) (n : ℕ),
  (p * q).coeff n = ∑ x ∈ Finset.HasAntidiagonal.antidiagonal n, p.coeff x.1 * q.coeff x.2
-- Mathlib.Algebra.Order.Interval.Set.Group
Set.pairwise_disjoint_Ioc_zpow : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α] (b : α),
  Pairwise (Function.onFun Disjoint fun n => Set.Ioc (b ^ n) (b ^ (n + 1)))
-- Mathlib.Data.LawfulXor.Basic
xor_right_eq_self_iff : ∀ {α : Type u_1} [inst : XorOp α] [inst_1 : Zero α] [LawfulXor α] {a b : α}, b ^^^ a = a ↔ b = 0
-- Mathlib.Algebra.Homology.Factorizations.CM5b
CochainComplex.cm5b.instMonoIntI : ∀ {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 ℤ} (f : K ⟶ L),
  CategoryTheory.Mono (CochainComplex.cm5b.i f)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.isSome_minKey?_eq_not_isEmpty : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp],
  t.minKey?.isSome = !t.isEmpty
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
SemimoduleCat.MonoidalCategory.tensorHom_def : ∀ {R : Type u} [inst : CommSemiring R] {X₁ Y₁ X₂ Y₂ : SemimoduleCat R} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂),
  CategoryTheory.MonoidalCategoryStruct.tensorHom f g = SemimoduleCat.MonoidalCategory.tensorHom f g
-- Mathlib.Tactic.TypeStar
/-- The syntax `variable (X Y ... Z : Sort*)` creates a new distinct implicit universe variable
for each variable in the sequence.  -/
Lean.Elab.Term.«termSort*» : Lean.ParserDescr
-- Mathlib.AlgebraicGeometry.AffineTransitionLimit
AlgebraicGeometry.Scheme.exists_hom_comp_eq_comp_of_locallyOfFiniteType : ∀ {I : Type u} [inst : CategoryTheory.Category.{u, u} I] {S X : AlgebraicGeometry.Scheme}
  (D : CategoryTheory.Functor I AlgebraicGeometry.Scheme) (t : D ⟶ (CategoryTheory.Functor.const I).obj S) (f : X ⟶ S)
  (c : CategoryTheory.Limits.Cone D) (hc : CategoryTheory.Limits.IsLimit c) [∀ (i : I), CompactSpace ↥(D.obj i)]
  [AlgebraicGeometry.LocallyOfFiniteType f] [CategoryTheory.IsCofiltered I]
  [∀ {i j : I} (f : i ⟶ j), AlgebraicGeometry.IsAffineHom (D.map f)] {i : I} (a b : D.obj i ⟶ X),
  t.app i = CategoryTheory.CategoryStruct.comp a f →
    t.app i = CategoryTheory.CategoryStruct.comp b f →
      CategoryTheory.CategoryStruct.comp (c.π.app i) a = CategoryTheory.CategoryStruct.comp (c.π.app i) b →
        ∃ k hik, CategoryTheory.CategoryStruct.comp (D.map hik) a = CategoryTheory.CategoryStruct.comp (D.map hik) b
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
Std.IterM.anyM_eq_forIn : ∀ {α β : Type w} {m : Type w → Type w'} [inst : Std.Iterator α m β] [Std.Iterators.Finite α m] [inst_2 : Monad m]
  [LawfulMonad m] [inst_4 : Std.IteratorLoop α m m] [Std.LawfulIteratorLoop α m m] {it : Std.IterM m β}
  {p : β → m (ULift.{w, 0} Bool)},
  Std.IterM.anyM p it =
    forIn it { down := false } fun x x_1 => do
      let __do_lift ← p x
      if __do_lift.down = true then pure (ForInStep.done { down := true }) else pure (ForInStep.yield { down := false })
-- Mathlib.Analysis.Convex.Join
subset_convexJoin_left : ∀ {𝕜 : Type u_2} {E : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : Module 𝕜 E] {s t : Set E} [IsOrderedRing 𝕜], t.Nonempty → s ⊆ convexJoin 𝕜 s t
-- Init.Data.Array.Monadic
_private.Init.Data.Array.Monadic.0.List.foldlM_filterMap.match_1.splitter : {β : Type u_1} →
  (motive : Option β → Sort u_2) → (x : Option β) → ((b : β) → motive (some b)) → (Unit → motive none) → motive x
-- Mathlib.Order.Filter.Bases.Basic
Filter.HasBasis.coprod : ∀ {α : Type u_1} {β : Type u_2} {la : Filter α} {lb : Filter β} {ι : Type u_6} {ι' : Type u_7} {pa : ι → Prop}
  {sa : ι → Set α} {pb : ι' → Prop} {sb : ι' → Set β},
  la.HasBasis pa sa →
    lb.HasBasis pb sb →
      (la.coprod lb).HasBasis (fun i => pa i.1 ∧ pb i.2) fun i => Prod.fst ⁻¹' sa i.1 ∪ Prod.snd ⁻¹' sb i.2
-- Init.Data.String.PosRaw
String.endPos_empty : "".rawEndPos = 0
-- Mathlib.Topology.Algebra.Order.Field
inv_nhdsGT_zero : ∀ {𝕜 : Type u_1} [inst : Semifield 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [inst_3 : TopologicalSpace 𝕜]
  [OrderTopology 𝕜], (nhdsWithin 0 (Set.Ioi 0))⁻¹ = Filter.atTop
-- Mathlib.Topology.Bornology.BoundedOperation
isBounded_mul : ∀ {R : Type u_1} [inst : Bornology R] [inst_1 : Mul R] [BoundedMul R] {s t : Set R},
  Bornology.IsBounded s → Bornology.IsBounded t → Bornology.IsBounded (s * t)
-- Mathlib.Analysis.Complex.Trigonometric
Complex.cos_conj : ∀ (x : ℂ), Complex.cos ((starRingEnd ℂ) x) = (starRingEnd ℂ) (Complex.cos x)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.Equiv.inter_left : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ m₃ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → m₃.WF → m₁.Equiv m₂ → (m₁ ∩ m₃).Equiv (m₂ ∩ m₃)
-- Mathlib.Data.Nat.Size
Nat.size_shiftLeft' : ∀ {b : Bool} {m n : ℕ}, Nat.shiftLeft' b m n ≠ 0 → (Nat.shiftLeft' b m n).size = m.size + n
-- Mathlib.Data.Finset.Empty
Finset.eq_empty_of_forall_notMem : ∀ {α : Type u_1} {s : Finset α}, (∀ (x : α), x ∉ s) → s = ∅
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Expr.toPoly.eq_4 : ∀ (x_1 : Lean.Grind.CommRing.Var), (Lean.Grind.CommRing.Expr.var x_1).toPoly = Lean.Grind.CommRing.Poly.ofVar x_1
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenAddSubgroup.isClosed : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [SeparatelyContinuousAdd G] (U : OpenAddSubgroup G),
  IsClosed ↑U
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic
CFC.log_pow' : ∀ {A : Type u_1} [inst : NormedRing A] [inst_1 : StarRing A] [inst_2 : NormedAlgebra ℝ A]
  [inst_3 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_4 : PartialOrder A] [StarOrderedRing A]
  [NonnegSpectrumClass ℝ A] (n : ℕ) (a : A),
  autoParam (IsStrictlyPositive a) CFC.log_pow'._auto_1 → CFC.log (a ^ n) = n • CFC.log a
-- Mathlib.Topology.OpenPartialHomeomorph.Composition
Homeomorph.transOpenPartialHomeomorph_eq_trans : ∀ {X : Type u_1} {Y : Type u_3} {Z : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] (e : X ≃ₜ Y) (f' : OpenPartialHomeomorph Y Z),
  e.transOpenPartialHomeomorph f' = e.toOpenPartialHomeomorph.trans f'
-- Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
/-- An angle in a right-angled triangle expressed using `arccos`.  -/
Orientation.oangle_add_right_eq_arccos_of_oangle_eq_pi_div_two : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [hd2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y : V},
  o.oangle x y = ↑(Real.pi / 2) → o.oangle x (x + y) = ↑(Real.arccos (‖x‖ / ‖x + y‖))
-- Mathlib.Topology.Compactness.SigmaCompact
instSigmaCompactSpaceSum : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [SigmaCompactSpace X]
  [SigmaCompactSpace Y], SigmaCompactSpace (X ⊕ Y)
-- Mathlib.Combinatorics.Graph.Delete
/-- The graph obtained from `G` by deleting a set of vertices.  -/
Graph.deleteVerts : {α : Type u_1} → {β : Type u_2} → Graph α β → Set α → Graph α β
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
/-- The left homology map data associated to the zero morphism between two short complexes.  -/
CategoryTheory.ShortComplex.LeftHomologyMapData.zero : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S₁ S₂ : CategoryTheory.ShortComplex C} →
        (h₁ : S₁.LeftHomologyData) →
          (h₂ : S₂.LeftHomologyData) → CategoryTheory.ShortComplex.LeftHomologyMapData 0 h₁ h₂
-- Mathlib.Algebra.Group.Submonoid.Defs
/-- A submonoid of a monoid inherits a multiplication.  -/
Submonoid.mul : {M : Type u_4} → [inst : MulOneClass M] → (S : Submonoid M) → Mul ↥S
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
/-- **Alias** of `Submodule.eq_starProjection_of_mem_of_inner_eq_zero`.

---

The orthogonal projection is the unique point in `K` with the
orthogonality property.  -/
Submodule.eq_orthogonalProjectionFn_of_mem_of_inner_eq_zero : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {K : Submodule 𝕜 E} [inst_3 : K.HasOrthogonalProjection] {u v : E},
  v ∈ K → (∀ w ∈ K, inner 𝕜 (u - v) w = 0) → K.starProjection u = v
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CompletionItemKind.ofNat : ℕ → Lean.Lsp.CompletionItemKind
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.basisFun_map : ∀ (p : ENNReal) (𝕜 : Type u_1) (ι : Type u_2) [inst : Finite ι] [inst_1 : Ring 𝕜],
  (PiLp.basisFun p 𝕜 ι).map (WithLp.linearEquiv p 𝕜 (ι → 𝕜)) = Pi.basisFun 𝕜 ι
-- Mathlib.RingTheory.WittVector.Truncated
WittVector.truncateFun_mul : ∀ {p : ℕ} (n : ℕ) {R : Type u_1} [inst : CommRing R] [inst_1 : Fact (Nat.Prime p)] (x y : WittVector p R),
  WittVector.truncateFun n (x * y) = WittVector.truncateFun n x * WittVector.truncateFun n y
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.toSubsemiring_inj : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] {S U : Subalgebra R A},
  S.toSubsemiring = U.toSubsemiring ↔ S = U
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgEquiv.one_apply : ∀ {S : Type u_1} {R : Type u_2} [inst : Mul R] [inst_1 : Add R] [inst_2 : Star R] [inst_3 : SMul S R] (x : R), 1 x = x
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get?_eq_some_get! : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : Inhabited β],
  t.WF → ∀ {a : α}, a ∈ t → Std.DTreeMap.Raw.Const.get? t a = some (Std.DTreeMap.Raw.Const.get! t a)
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.productTriangle.lift_hom₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ] {J : Type u_1}
  (T : J → CategoryTheory.Pretriangulated.Triangle C) [inst_2 : CategoryTheory.Limits.HasProduct fun j => (T j).obj₁]
  [inst_3 : CategoryTheory.Limits.HasProduct fun j => (T j).obj₂]
  [inst_4 : CategoryTheory.Limits.HasProduct fun j => (T j).obj₃]
  [inst_5 : CategoryTheory.Limits.HasProduct fun j => (CategoryTheory.shiftFunctor C 1).obj (T j).obj₁]
  {T' : CategoryTheory.Pretriangulated.Triangle C} (φ : (j : J) → T' ⟶ T j),
  (CategoryTheory.Pretriangulated.productTriangle.lift T φ).hom₁ = CategoryTheory.Limits.Pi.lift fun j => (φ j).hom₁
-- Mathlib.Algebra.Order.Archimedean.Class
FiniteMulArchimedeanClass.ballSubgroup_strictAnti : ∀ {M : Type u_1} [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M],
  StrictAnti FiniteMulArchimedeanClass.ballSubgroup
-- Lean.Elab.DocString
Lean.Doc.DocArg.str.inj : ∀ {val val_1 : Lean.StrLit}, Lean.Doc.DocArg.str val = Lean.Doc.DocArg.str val_1 → val = val_1
-- Lean.Meta.Sym.Simp.SimpM
Lean.Meta.Sym.Simp.Methods.mk.sizeOf_spec : ∀ (pre post : Lean.Meta.Sym.Simp.Simproc), sizeOf { pre := pre, post := post } = 1
-- Mathlib.Order.Heyting.Regular
/-- An element of a Heyting algebra is regular if its double complement is itself.  -/
Heyting.IsRegular : {α : Type u_1} → [Compl α] → α → Prop
-- Mathlib.MeasureTheory.MeasurableSpace.Card
MeasurableSpace.iUnion_mem_generateMeasurableRec : ∀ {α : Type u} {s : Set (Set α)} {i : Ordinal.{u_1}} {f : ℕ → Set α},
  (∀ (n : ℕ), ∃ j < i, f n ∈ MeasurableSpace.generateMeasurableRec s j) →
    ⋃ n, f n ∈ MeasurableSpace.generateMeasurableRec s i
-- Mathlib.Logic.Equiv.Finset
/-- If `α` is denumerable, then so is `Finset α`. Warning: this is *not* the same encoding as used
in `Finset.encodable`.  -/
Denumerable.finset : {α : Type u_1} → [Denumerable α] → Denumerable (Finset α)
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.toNonUnitalRingHom_refl : ∀ {R : Type u_4} [inst : NonUnitalNonAssocSemiring R], (RingEquiv.refl R).toNonUnitalRingHom = NonUnitalRingHom.id R
-- Mathlib.Algebra.Polynomial.PartialFractions
/-- Let `R` be a commutative ring and `f : R[X]`. Let `s` be a finite index set.
Let `g i` be a collection of monic and pairwise coprime polynomials indexed by `s`,
and for each `g i` let `n i` be a natural number. Then `f` can be written in the form
`(∏ i ∈ s, g i ^ n i) * (q + ∑ i ∈ s, ∑ j : Fin (n i), r i j / g i ^ (j + 1))`
in at most one way, where `degree (r i j) < degree (g i)` and the denominator cancels formally.
See `eq_quo_mul_prod_pow_add_sum_rem_mul_prod_pow` for the existence of such a representation.  -/
Polynomial.quo_mul_prod_pow_add_sum_rem_mul_prod_pow_unique : ∀ {R : Type u_1} [inst : CommRing R] {ι : Type u_2} [inst_1 : DecidableEq ι] {s : Finset ι} {g : ι → Polynomial R},
  (∀ i ∈ s, (g i).Monic) →
    ((↑s).Pairwise fun i j => IsCoprime (g i) (g j)) →
      ∀ {n : ι → ℕ} {q₁ q₂ : Polynomial R} {r₁ r₂ : (i : ι) → Fin (n i) → Polynomial R},
        (∀ i ∈ s, ∀ (j : Fin (n i)), (r₁ i j).degree < (g i).degree) →
          (∀ i ∈ s, ∀ (j : Fin (n i)), (r₂ i j).degree < (g i).degree) →
            q₁ * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, ∑ j, r₁ i j * g i ^ ↑j * ∏ k ∈ s.erase i, g k ^ n k =
                q₂ * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, ∑ j, r₂ i j * g i ^ ↑j * ∏ k ∈ s.erase i, g k ^ n k →
              q₁ = q₂ ∧ ∀ i ∈ s, r₁ i = r₂ i
-- Mathlib.Combinatorics.SimpleGraph.Prod
/-- The box product is commutative up to isomorphism. `Equiv.prodComm` as a graph isomorphism.  -/
SimpleGraph.boxProdComm : {α : Type u_1} → {β : Type u_2} → (G : SimpleGraph α) → (H : SimpleGraph β) → G □ H ≃g H □ G
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
StrictAnti.const_mul' : ∀ {α : Type u_1} {β : Type u_2} [inst : Mul α] [inst_1 : Preorder α] [inst_2 : Preorder β] {f : β → α}
  [MulLeftStrictMono α], StrictAnti f → ∀ (c : α), StrictAnti fun x => c * f x
-- Lean.Meta.Tactic.Backtrack
/-- Run a monadic function on every element of a list,
returning the list of elements on which the function fails, and the list of successful results.  -/
Lean.Meta.Tactic.Backtrack.Backtrack.tryAllM : {m : Type (max u_1 u_2) → Type u_3} →
  {α : Type u_2} → {β : Type (max u_1 u_2)} → [Monad m] → [Alternative m] → List α → (α → m β) → m (List α × List β)
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
Real.log_lt_sub_one_of_pos : ∀ {x : ℝ}, 0 < x → x ≠ 1 → Real.log x < x - 1
-- Mathlib.Analysis.Normed.Algebra.Spectrum
spectrum.mem_resolventSet_of_spectralRadius_lt : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NormedField 𝕜] [inst_1 : Ring A] [inst_2 : Algebra 𝕜 A] {a : A} {k : 𝕜},
  spectralRadius 𝕜 a < ↑‖k‖₊ → k ∈ resolventSet 𝕜 a
-- Lean.Meta.Tactic.Grind.Arith.Linear.Util
Lean.Meta.Grind.Arith.Linear.getLEInst : Lean.Meta.Grind.Arith.Linear.LinearM Lean.Expr
-- Mathlib.Analysis.Asymptotics.Theta
Asymptotics.instTransForallEventuallyEqIsTheta : {α : Type u_1} →
  {E : Type u_3} →
    {F : Type u_4} →
      [inst : Norm E] →
        [inst_1 : Norm F] → {l : Filter α} → Trans l.EventuallyEq (Asymptotics.IsTheta l) (Asymptotics.IsTheta l)
-- Mathlib.Topology.Algebra.UniformMulAction
UniformSpace.Completion.instIsCentralVAdd : ∀ (M : Type v) (X : Type x) [inst : UniformSpace X] [inst_1 : VAdd M X] [inst_2 : VAdd Mᵃᵒᵖ X] [IsCentralVAdd M X],
  IsCentralVAdd M (UniformSpace.Completion X)
-- Init.Data.Array.Basic
_private.Init.Data.Array.Basic.0.Array.ext.extAux : ∀ {α : Type u} (as bs : List α),
  as.length = bs.length → (∀ (i : ℕ) (hi₁ : i < as.length) (hi₂ : i < bs.length), as[i] = bs[i]) → as = bs
-- Mathlib.AlgebraicGeometry.StructureSheaf
_private.Mathlib.AlgebraicGeometry.StructureSheaf.0.AlgebraicGeometry.StructureSheaf.toBasicOpenₗ_surjective : ∀ {R M : Type u} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (f : R),
  Function.Surjective ⇑(AlgebraicGeometry.StructureSheaf.toBasicOpenₗ✝ R M f)
-- Mathlib.RingTheory.DividedPowerAlgebra.Init
DividedPowerAlgebra.Rel.zero : ∀ {R : Type u_2} {M : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {a : M},
  DividedPowerAlgebra.Rel R M (MvPolynomial.X (0, a)) 1
-- Mathlib.Analysis.Complex.Trigonometric
Complex.ofReal_sinh_ofReal_re : ∀ (x : ℝ), ↑(Complex.sinh ↑x).re = Complex.sinh ↑x
-- Mathlib.MeasureTheory.Integral.Average
MeasureTheory.laverage_union_mem_openSegment : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α} {f : α → ENNReal},
  MeasureTheory.AEDisjoint μ s t →
    MeasureTheory.NullMeasurableSet t μ →
      μ s ≠ 0 →
        μ t ≠ 0 →
          μ s ≠ ⊤ →
            μ t ≠ ⊤ →
              ⨍⁻ (x : α) in s ∪ t, f x ∂μ ∈ openSegment ENNReal (⨍⁻ (x : α) in s, f x ∂μ) (⨍⁻ (x : α) in t, f x ∂μ)
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.integrable_of_integral_eq_one : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ},
  ∫ (x : α), f x ∂μ = 1 → MeasureTheory.Integrable f μ
-- Lean.Elab.Tactic.Omega.Core
/-- The coefficients for which `constraints` contains an exact constraint (i.e. an equality).
 -/
Lean.Elab.Tactic.Omega.Problem.equalities : Lean.Elab.Tactic.Omega.Problem → Std.HashSet Lean.Omega.Coeffs
-- Mathlib.RingTheory.Algebraic.Cardinality
/-- The cardinality of an algebraic extension is at most the maximum of the cardinality
of the base ring or `ℵ₀`.  -/
Algebra.IsAlgebraic.cardinalMk_le_max : ∀ (R : Type u) [inst : CommRing R] [IsDomain R] (L : Type u) [inst_2 : CommRing L] [IsDomain L] [inst_4 : Algebra R L]
  [Module.IsTorsionFree R L] [Algebra.IsAlgebraic R L], Cardinal.mk L ≤ max (Cardinal.mk R) Cardinal.aleph0
-- Mathlib.RingTheory.Finiteness.Basic
RingHom.Finite.instFinite : ∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : CommRing B] (h : A ≃+* B), Module.Finite A B
-- Mathlib.Algebra.Homology.Embedding.TruncGE
HomologicalComplex.truncGE'Map_comp : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {K L M : HomologicalComplex C c'} (φ : K ⟶ L) (φ' : L ⟶ M) (e : c.Embedding c') [inst_2 : e.IsTruncGE]
  [inst_3 : ∀ (i' : ι'), K.HasHomology i'] [inst_4 : ∀ (i' : ι'), L.HasHomology i']
  [inst_5 : ∀ (i' : ι'), M.HasHomology i'],
  HomologicalComplex.truncGE'Map (CategoryTheory.CategoryStruct.comp φ φ') e =
    CategoryTheory.CategoryStruct.comp (HomologicalComplex.truncGE'Map φ e) (HomologicalComplex.truncGE'Map φ' e)
-- Mathlib.Algebra.BigOperators.Group.Finset.Indicator
/-- Consider a sum of `g i (f i)` over a finset.  Suppose `g` is a function such as
`n ↦ (n • ·)`, which maps a second argument of `0` to `0` (or a weighted sum of `f i * h i` or
`f i • h i`, where `f` gives the weights that are multiplied by some other function `h`). Then if
`f` is replaced by the corresponding indicator function, the finset may be replaced by a possibly
larger finset without changing the value of the sum.  -/
Finset.sum_indicator_subset_of_eq_zero : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : AddCommMonoid β] [inst_1 : Zero α] (f : ι → α) (g : ι → α → β)
  {s t : Finset ι}, s ⊆ t → (∀ (a : ι), g a 0 = 0) → ∑ i ∈ t, g i ((↑s).indicator f i) = ∑ i ∈ s, g i (f i)
-- Init.Data.List.Basic
/-- Removes the element at the specified index. If the index is out of bounds, the list is returned
unmodified.

`O(i)`.

Examples:
* `[0, 1, 2, 3, 4].eraseIdx 0 = [1, 2, 3, 4]`
* `[0, 1, 2, 3, 4].eraseIdx 1 = [0, 2, 3, 4]`
* `[0, 1, 2, 3, 4].eraseIdx 5 = [0, 1, 2, 3, 4]`
 -/
List.eraseIdx : {α : Type u} → List α → ℕ → List α
-- Mathlib.Topology.Algebra.ContinuousAffineEquiv
ContinuousAffineEquiv.pointReflection_symm : ∀ (k : Type u_1) {P₁ : Type u_2} {V₁ : Type u_6} [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁]
  [inst_3 : AddTorsor V₁ P₁] [inst_4 : TopologicalSpace P₁] [inst_5 : TopologicalSpace V₁]
  [inst_6 : IsTopologicalAddTorsor P₁] (x : P₁),
  (ContinuousAffineEquiv.pointReflection k x).symm = ContinuousAffineEquiv.pointReflection k x
-- Mathlib.Topology.Order.AtTopBotIxx
tendsto_comp_coe_Iio_atTop : ∀ {X : Type u_1} [inst : LinearOrder X] [inst_1 : TopologicalSpace X] [OrderTopology X] {a : X} {α : Type u_2}
  {l : Filter α} {f : X → α},
  autoParam (Order.IsSuccPrelimit a) tendsto_comp_coe_Iio_atTop._auto_1 →
    (Filter.Tendsto (fun x => f ↑x) Filter.atTop l ↔ Filter.Tendsto f (nhdsWithin a (Set.Iio a)) l)
-- Lean.Compiler.LCNF.Basic
_private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.Code.sizeLe.go : {pu : Lean.Compiler.LCNF.Purity} → ℕ → Lean.Compiler.LCNF.Code pu → EStateM Unit ℕ Unit
-- Std.Data.HashMap.Iterator
/-- Returns a finite iterator over the entries of a hash map.
The iterator yields the elements of the map in order and then terminates.

**Termination properties:**

* `Finite` instance: always
* `Productive` instance: always
 -/
Std.HashMap.valuesIter : {α β : Type u} → [inst : BEq α] → [inst_1 : Hashable α] → Std.HashMap α β → Std.Iter β
-- Mathlib.SetTheory.Cardinal.ENat
Cardinal.toENatAux_gc : GaloisConnection Cardinal.ofENat Cardinal.toENatAux
-- Mathlib.Combinatorics.Matroid.Constructions
Matroid.loopyOn_isBase_iff : ∀ {α : Type u_1} {E B : Set α}, (Matroid.loopyOn E).IsBase B ↔ B = ∅
-- Mathlib.LinearAlgebra.LinearPMap
LinearPMap.mkSpanSingleton_apply : ∀ (K : Type u_7) (L : Type u_8) {E : Type u_9} {F : Type u_10} [inst : DivisionRing K] [inst_1 : DivisionRing L]
  {σ : K →+* L} [inst_2 : AddCommGroup E] [inst_3 : Module K E] [inst_4 : AddCommGroup F] [inst_5 : Module L F] {x : E}
  (hx : x ≠ 0) (y : F), ↑(LinearPMap.mkSpanSingleton x y hx) ⟨x, ⋯⟩ = y
-- Std.Data.Iterators.Lemmas.Producers.Range
Std.Ric.count_iter : ∀ {α : Type u_1} [inst : Std.PRange.Least? α] [inst_1 : LE α] [inst_2 : DecidableLE α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerableLE α] [Std.Rxc.IsAlwaysFinite α]
  [inst_6 : Std.PRange.LawfulUpwardEnumerable α] [inst_7 : Std.Rxc.HasSize α] [Std.Rxc.LawfulHasSize α] {r : Std.Ric α},
  r.iter.length = r.size
-- Init.GrindInstances.Ring.UInt
UInt32.instOfNat.eq_1 : ∀ {n : ℕ}, UInt32.instOfNat = { ofNat := UInt32.ofNat n }
-- Mathlib.Topology.Path
Path.id_apply : ∀ (a : ↑unitInterval), Path.id a = a