mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.AddMod.assoc_flip : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D]
  {A : C} [inst_4 : CategoryTheory.AddMonObj A] (M : CategoryTheory.AddMod D A),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight A CategoryTheory.AddModObj.vadd)
      CategoryTheory.AddModObj.vadd =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso A A M.X).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft CategoryTheory.AddMonObj.add M.X)
        CategoryTheory.AddModObj.vadd)
-- Mathlib.FieldTheory.Perfect
coe_frobeniusEquiv : ∀ (R : Type u_1) (p : ℕ) [inst : CommSemiring R] [inst_1 : ExpChar R p] [inst_2 : PerfectRing R p],
  ⇑(frobeniusEquiv R p) = ⇑(frobenius R p)
-- Mathlib.AlgebraicGeometry.Gluing
AlgebraicGeometry.Scheme.Cover.idx.eq_1 : ∀ {K : CategoryTheory.Precoverage AlgebraicGeometry.Scheme} {X : AlgebraicGeometry.Scheme}
  [inst : AlgebraicGeometry.Scheme.JointlySurjective K] (𝒰 : AlgebraicGeometry.Scheme.Cover K X) (x : ↥X),
  𝒰.idx x = ⋯.choose
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero
CategoryTheory.Functor.preservesZeroMorphisms_of_map_zero_object : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.Limits.HasZeroObject D]
  [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_5 : CategoryTheory.Limits.HasZeroMorphisms D]
  {F : CategoryTheory.Functor C D} (i : F.obj 0 ≅ 0), F.PreservesZeroMorphisms
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey!_eq_get!_getKey? : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  [inst : Inhabited α] {a : α}, m.getKey! a = (m.getKey? a).get!
-- Init.Data.Iterators.Basic
/-- Termination measure to be used in well-founded recursive functions recursing over a finite iterator
(see also `Finite`).
 -/
Std.Iter.finitelyManySteps : {α β : Type w} →
  [inst : Std.Iterator α Id β] → [Std.Iterators.Finite α Id] → Std.Iter β → Std.IterM.TerminationMeasures.Finite α Id
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
ENNReal.rpow_eq_top_of_nonneg : ∀ (x : ENNReal) {y : ℝ}, 0 ≤ y → x ^ y = ⊤ → x = ⊤
-- Mathlib.Geometry.Manifold.Algebra.Monoid
contMDiff_pow : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {H : Type u_2} [inst_1 : TopologicalSpace H]
  {E : Type u_3} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4}
  [inst_4 : Monoid G] [inst_5 : TopologicalSpace G] [inst_6 : ChartedSpace H G] [ContMDiffMul I n G] (i : ℕ),
  ContMDiff I I n fun a => a ^ i
-- Mathlib.Analysis.Asymptotics.ExpGrowth
/-- See `le_expGrowthSup_mul` for a version with swapped argument `u` and `v`.  -/
ExpGrowth.le_expGrowthSup_mul' : ∀ {u v : ℕ → ENNReal}, ExpGrowth.expGrowthInf u + ExpGrowth.expGrowthSup v ≤ ExpGrowth.expGrowthSup (u * v)
-- Mathlib.Analysis.Normed.Field.Basic
NormedField.nhdsNE_neBot : ∀ {α : Type u_2} [inst : NontriviallyNormedField α] (x : α), (nhdsWithin x {x}ᶜ).NeBot
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.X_pow_mul_monomial : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : MulSemiringAction (Multiplicative ℕ) R] (k n : ℕ) (r : R),
  SkewPolynomial.X ^ k * (SkewPolynomial.monomial n) r = (SkewPolynomial.monomial (n + k)) ((⇑SkewPolynomial.φ)^[k] r)
-- Lean.Elab.Tactic.Try
/-- `evalSuggest` for `attempt_all` tactic.  -/
_private.Lean.Elab.Tactic.Try.0.Lean.Elab.Tactic.Try.evalSuggestAttemptAll : Array (Lean.TSyntax `Lean.Parser.Tactic.tacticSeq) → Lean.Elab.Tactic.Try.TryTacticM (Lean.TSyntax `tactic)
-- Init.Data.String.Basic
ByteArray.utf8Encode_get_utf8Decode? : ∀ {b : ByteArray} {h : b.utf8Decode?.isSome = true}, (b.utf8Decode?.get h).toList.utf8Encode = b
-- Mathlib.Tactic.Explode.Datatypes
/-- What to display in the "theorem applied" column.
Make sure to use `addMessageContext` if needed.  -/
Mathlib.Explode.Entry.thm : Mathlib.Explode.Entry → Lean.MessageData
-- Mathlib.AlgebraicTopology.RelativeCellComplex.AttachCells
HomotopicalAlgebra.AttachCells.reindex_cofan₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {α : Type t} {A B : α → C} {g : (a : α) → A a ⟶ B a}
  {X₁ X₂ : C} {f : X₁ ⟶ X₂} (c : HomotopicalAlgebra.AttachCells g f) {ι' : Type w'} (e : ι' ≃ c.ι),
  (c.reindex e).cofan₁ = CategoryTheory.Limits.Cofan.mk c.cofan₁.pt fun i' => c.cofan₁.inj (e i')
-- Mathlib.Geometry.Manifold.Algebra.Monoid
instMonoidHomClassContMDiffMonoidMorphism : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {H : Type u_2} [inst_1 : TopologicalSpace H]
  {E : Type u_3} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4}
  [inst_4 : Monoid G] [inst_5 : TopologicalSpace G] [inst_6 : ChartedSpace H G] {H' : Type u_5}
  [inst_7 : TopologicalSpace H'] {E' : Type u_6} [inst_8 : NormedAddCommGroup E'] [inst_9 : NormedSpace 𝕜 E']
  {I' : ModelWithCorners 𝕜 E' H'} {G' : Type u_7} [inst_10 : Monoid G'] [inst_11 : TopologicalSpace G']
  [inst_12 : ChartedSpace H' G'], MonoidHomClass (ContMDiffMonoidMorphism I I' n G G') G G'
-- Mathlib.MeasureTheory.Function.LpSpace.Indicator
/-- The `eLpNorm` of the indicator of a set is uniformly small if the set itself has small measure,
for any `p < ∞`. Given here as an existential `∀ ε > 0, ∃ η > 0, ...` to avoid later
management of `ℝ≥0∞`-arithmetic.  -/
MeasureTheory.exists_eLpNorm_indicator_le : ∀ {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E],
  p ≠ ⊤ →
    ∀ (c : E) {ε : ENNReal},
      ε ≠ 0 → ∃ η, 0 < η ∧ ∀ (s : Set α), μ s ≤ ↑η → MeasureTheory.eLpNorm (s.indicator fun x => c) p μ ≤ ε
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.size_le_size_insertIfNew : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β}, t.size ≤ (t.insertIfNew k v).size
-- Mathlib.Algebra.MvPolynomial.Equiv
MvPolynomial.sumAlgEquiv_C_inl : ∀ (R : Type u) (S₁ : Type v) (S₂ : Type w) [inst : CommSemiring R] (r : R),
  (MvPolynomial.sumAlgEquiv R S₁ S₂) (MvPolynomial.C r) = MvPolynomial.C (MvPolynomial.C r)
-- Mathlib.Logic.Small.Defs
/-- The noncomputable equivalence between a `w`-small type and a model.
 -/
equivShrink : (α : Type v) → [inst : Small.{w, v} α] → α ≃ Shrink.{w, v} α
-- Mathlib.Geometry.Convex.Cone.Pointed
PointedCone.mem_lineal : ∀ {R : Type u_1} {E : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommGroup E] [inst_4 : Module R E] {C : PointedCone R E} {x : E}, x ∈ C.lineal ↔ x ∈ C ∧ -x ∈ C
-- Mathlib.Analysis.Convex.StdSimplex
stdSimplex_eq_inter : ∀ (𝕜 : Type u_2) (ι : Type u_1) [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : Fintype ι],
  stdSimplex 𝕜 ι = (⋂ x, {f | 0 ≤ f x}) ∩ {f | ∑ x, f x = 1}
-- Mathlib.Algebra.Polynomial.FieldDivision
Polynomial.C_mul_dvd : ∀ {R : Type u} {a : R} [inst : Field R] {p q : Polynomial R}, a ≠ 0 → (Polynomial.C a * p ∣ q ↔ p ∣ q)
-- Mathlib.FieldTheory.Finite.GaloisField
FiniteField.natCard_algHom_of_finrank_dvd : ∀ {F : Type u_3} {K : Type u_4} {L : Type u_5} [inst : Field F] [inst_1 : Field K] [inst_2 : Algebra F K]
  [inst_3 : Field L] [inst_4 : Algebra F L] [Finite L],
  Module.finrank F K ∣ Module.finrank F L → Nat.card (K →ₐ[F] L) = Module.finrank F K
-- Mathlib.Algebra.IsPrimePow
/-- An equivalent definition for prime powers: `n` is a prime power iff there is a prime `p` and a
natural `k` such that `n` can be written as `p^(k+1)`.  -/
isPrimePow_iff_pow_succ : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] (n : R), IsPrimePow n ↔ ∃ p k, Prime p ∧ p ^ (k + 1) = n
-- Mathlib.Combinatorics.Graph.Simple
Graph.IsLoopAt.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (G : Graph α β) (e : β) (x : α), G.IsLoopAt e x = G.IsLink e x x
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.Homotopy.mk.inj : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {inst_1 : CategoryTheory.Preadditive C}
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ₁ φ₂ : S₁ ⟶ S₂} {h₀ : S₁.X₁ ⟶ S₂.X₁}
  {h₀_f :
    autoParam (CategoryTheory.CategoryStruct.comp h₀ S₂.f = 0) CategoryTheory.ShortComplex.Homotopy.h₀_f._autoParam}
  {h₁ : S₁.X₂ ⟶ S₂.X₁} {h₂ : S₁.X₃ ⟶ S₂.X₂} {h₃ : S₁.X₃ ⟶ S₂.X₃}
  {g_h₃ :
    autoParam (CategoryTheory.CategoryStruct.comp S₁.g h₃ = 0) CategoryTheory.ShortComplex.Homotopy.g_h₃._autoParam}
  {comm₁ :
    autoParam (φ₁.τ₁ = CategoryTheory.CategoryStruct.comp S₁.f h₁ + h₀ + φ₂.τ₁)
      CategoryTheory.ShortComplex.Homotopy.comm₁._autoParam}
  {comm₂ :
    autoParam (φ₁.τ₂ = CategoryTheory.CategoryStruct.comp S₁.g h₂ + CategoryTheory.CategoryStruct.comp h₁ S₂.f + φ₂.τ₂)
      CategoryTheory.ShortComplex.Homotopy.comm₂._autoParam}
  {comm₃ :
    autoParam (φ₁.τ₃ = h₃ + CategoryTheory.CategoryStruct.comp h₂ S₂.g + φ₂.τ₃)
      CategoryTheory.ShortComplex.Homotopy.comm₃._autoParam}
  {h₀_1 : S₁.X₁ ⟶ S₂.X₁}
  {h₀_f_1 :
    autoParam (CategoryTheory.CategoryStruct.comp h₀_1 S₂.f = 0) CategoryTheory.ShortComplex.Homotopy.h₀_f._autoParam}
  {h₁_1 : S₁.X₂ ⟶ S₂.X₁} {h₂_1 : S₁.X₃ ⟶ S₂.X₂} {h₃_1 : S₁.X₃ ⟶ S₂.X₃}
  {g_h₃_1 :
    autoParam (CategoryTheory.CategoryStruct.comp S₁.g h₃_1 = 0) CategoryTheory.ShortComplex.Homotopy.g_h₃._autoParam}
  {comm₁_1 :
    autoParam (φ₁.τ₁ = CategoryTheory.CategoryStruct.comp S₁.f h₁_1 + h₀_1 + φ₂.τ₁)
      CategoryTheory.ShortComplex.Homotopy.comm₁._autoParam}
  {comm₂_1 :
    autoParam
      (φ₁.τ₂ = CategoryTheory.CategoryStruct.comp S₁.g h₂_1 + CategoryTheory.CategoryStruct.comp h₁_1 S₂.f + φ₂.τ₂)
      CategoryTheory.ShortComplex.Homotopy.comm₂._autoParam}
  {comm₃_1 :
    autoParam (φ₁.τ₃ = h₃_1 + CategoryTheory.CategoryStruct.comp h₂_1 S₂.g + φ₂.τ₃)
      CategoryTheory.ShortComplex.Homotopy.comm₃._autoParam},
  { h₀ := h₀, h₀_f := h₀_f, h₁ := h₁, h₂ := h₂, h₃ := h₃, g_h₃ := g_h₃, comm₁ := comm₁, comm₂ := comm₂,
        comm₃ := comm₃ } =
      { h₀ := h₀_1, h₀_f := h₀_f_1, h₁ := h₁_1, h₂ := h₂_1, h₃ := h₃_1, g_h₃ := g_h₃_1, comm₁ := comm₁_1,
        comm₂ := comm₂_1, comm₃ := comm₃_1 } →
    h₀ = h₀_1 ∧ h₁ = h₁_1 ∧ h₂ = h₂_1 ∧ h₃ = h₃_1
-- Mathlib.Algebra.Homology.ExactSequenceFour
CategoryTheory.ComposableArrows.IsComplex.opcyclesToCycles_fac_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {n : ℕ} {S : CategoryTheory.ComposableArrows C (n + 3)} (hS : S.IsComplex) (k : ℕ)
  (hk : autoParam (k ≤ n) CategoryTheory.ComposableArrows.IsComplex.opcyclesToCycles_fac._auto_1)
  [inst_2 : (S.sc hS k ⋯).HasRightHomology] [inst_3 : (S.sc hS (k + 1) ⋯).HasLeftHomology] {Z : C}
  (h : S.obj ⟨k + 1 + 1, ⋯⟩ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (S.sc hS k ⋯).pOpcycles
      (CategoryTheory.CategoryStruct.comp (hS.opcyclesToCycles k ⋯)
        (CategoryTheory.CategoryStruct.comp (S.sc hS (k + 1) ⋯).iCycles h)) =
    CategoryTheory.CategoryStruct.comp (S.map' (k + 1) (k + 2) ⋯ ⋯) h
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Maps
/-- **Alias** of the reverse direction of `HomogeneousIdeal.map_le_iff_le_comap`. -/
HomogeneousIdeal.map_le_of_le_comap : ∀ {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 𝒜} {J : HomogeneousIdeal ℬ},
  I ≤ HomogeneousIdeal.comap f J → HomogeneousIdeal.map f I ≤ J
-- Mathlib.Topology.VectorBundle.ContinuousAlternatingMap
Bundle.Trivialization.baseSet_continuousAlternatingMap : ∀ {𝕜 : Type u_1} {ι : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : Fintype ι] {B : Type u_3}
  [inst_2 : TopologicalSpace B] {F₁ : Type u_4} [inst_3 : NormedAddCommGroup F₁] [inst_4 : NormedSpace 𝕜 F₁]
  {E₁ : B → Type u_5} [inst_5 : (x : B) → AddCommGroup (E₁ x)] [inst_6 : (x : B) → Module 𝕜 (E₁ x)]
  [inst_7 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)] [inst_8 : (x : B) → TopologicalSpace (E₁ x)]
  [inst_9 : FiberBundle F₁ E₁] [inst_10 : VectorBundle 𝕜 F₁ E₁] {F₂ : Type u_6} [inst_11 : NormedAddCommGroup F₂]
  [inst_12 : NormedSpace 𝕜 F₂] {E₂ : B → Type u_7} [inst_13 : (x : B) → AddCommGroup (E₂ x)]
  [inst_14 : (x : B) → Module 𝕜 (E₂ x)] [inst_15 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)]
  [inst_16 : (x : B) → TopologicalSpace (E₂ x)] [inst_17 : FiberBundle F₂ E₂] [inst_18 : VectorBundle 𝕜 F₂ E₂]
  [inst_19 : ∀ (x : B), IsTopologicalAddGroup (E₂ x)] [inst_20 : ∀ (x : B), ContinuousSMul 𝕜 (E₂ x)]
  {e₁ : Bundle.Trivialization F₁ Bundle.TotalSpace.proj} {e₂ : Bundle.Trivialization F₂ Bundle.TotalSpace.proj}
  [he₁ : MemTrivializationAtlas e₁] [he₂ : MemTrivializationAtlas e₂],
  (Bundle.Trivialization.continuousAlternatingMap 𝕜 ι e₁ e₂).baseSet = e₁.baseSet ∩ e₂.baseSet
-- Mathlib.Analysis.Calculus.ContDiff.Defs
iteratedFDerivWithin_subset : ∀ {𝕜 : 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 t : Set E}
  {f : E → F} {x : E} {n : ℕ},
  s ⊆ t →
    UniqueDiffOn 𝕜 s →
      UniqueDiffOn 𝕜 t → ContDiffOn 𝕜 (↑n) f t → x ∈ s → iteratedFDerivWithin 𝕜 n f s x = iteratedFDerivWithin 𝕜 n f t x
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
/-- A `Simplex k P n` is a collection of `n + 1` affinely
independent points.  -/
Affine.Simplex : (k : Type u_1) →
  {V : Type u_2} →
    (P : Type u_5) → [inst : Ring k] → [inst_1 : AddCommGroup V] → [Module k V] → [AddTorsor V P] → ℕ → Type u_5
-- Mathlib.Algebra.Group.Equiv.TypeTags
AddEquiv.toMultiplicativeLeft_symm_apply_symm_apply : ∀ {G : Type u_2} {H : Type u_3} [inst : AddZeroClass G] [inst_1 : MulOneClass H] (f : Multiplicative G ≃* H)
  (a : Additive H), (AddEquiv.toMultiplicativeLeft.symm f).symm a = (MonoidHom.toAdditiveLeft f.symm.toMonoidHom) a
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
Std.IterM.up_length_toList_eq_length : ∀ {m : Type w → Type u_1} {α β : 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 β},
  (fun x => { down := x.length }) <$> it.toList = it.length
-- Lean.Data.Position
Lean.FileMap.ofString : String → Lean.FileMap
-- Init.Data.UInt.Lemmas
USize.toUInt8_eq : ∀ (a b : USize), a.toUInt8 = b.toUInt8 ↔ a % 256 = b % 256
-- Init.Data.Bool
Bool.and_or_inj_left : ∀ {m x y : Bool}, (m && x) = (m && y) → (m || x) = (m || y) → x = y
-- Mathlib.GroupTheory.Solvable
/-- A group `G` is solvable if its derived series is eventually trivial.  -/
Group.IsSolvable.solvable : ∀ {G : Type u_1} {inst : Group G} [self : Group.IsSolvable G], ∃ n, derivedSeries G n = ⊥
-- Std.Tactic.BVDecide.LRAT.Internal.Entails
Std.Tactic.BVDecide.LRAT.Internal.liff_unsat : ∀ {α : Type u} {σ1 : Type v} {σ2 : Type w} [inst : Std.Tactic.BVDecide.LRAT.Internal.Entails α σ1]
  [inst_1 : Std.Tactic.BVDecide.LRAT.Internal.Entails α σ2] (f1 : σ1) (f2 : σ2),
  Std.Tactic.BVDecide.LRAT.Internal.Liff α f1 f2 →
    (Std.Tactic.BVDecide.LRAT.Internal.Unsatisfiable α f1 ↔ Std.Tactic.BVDecide.LRAT.Internal.Unsatisfiable α f2)
-- Mathlib.Order.Interval.Finset.Basic
Finset.Ioi_subset_Ici_self : ∀ {α : Type u_2} [inst : Preorder α] [inst_1 : LocallyFiniteOrderTop α] {a : α}, Finset.Ioi a ⊆ Finset.Ici a
-- Mathlib.Analysis.MeanInequalitiesPow
/-- A constant for the inequality `‖f + g‖_{L^p} ≤ C * (‖f‖_{L^p} + ‖g‖_{L^p})`. It is equal to `1`
for `p ≥ 1` or `p = 0`, and `2^(1/p-1)` in the more tricky interval `(0, 1)`.  -/
ENNReal.LpAddConst : ENNReal → ENNReal
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.congrLeft_counitIso_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (e : C ≌ D) (X : CategoryTheory.Functor D E),
  e.congrLeft.counitIso.hom.app X = (e.invFunIdAssoc X).hom
-- Mathlib.Combinatorics.SimpleGraph.UniversalVerts
/-- The subgraph of `G` with the universal vertices removed.
 -/
SimpleGraph.deleteUniversalVerts : {V : Type u_1} → (G : SimpleGraph V) → G.Subgraph
-- Mathlib.Data.List.Basic
List.replicate_right_injective : ∀ {α : Type u} {n : ℕ}, n ≠ 0 → Function.Injective (List.replicate n)
-- Mathlib.MeasureTheory.SpecificCodomains.ContinuousMap
/-- A variant of `ContinuousMap.hasFiniteIntegral_mkD_of_bound` for a family of
functions which are continuous on a compact set.  -/
ContinuousMap.hasFiniteIntegral_mkD_restrict_of_bound : ∀ {X : Type u_1} {Y : Type u_2} [inst : MeasurableSpace X] {μ : MeasureTheory.Measure X} [inst_1 : TopologicalSpace Y]
  {E : Type u_3} [inst_2 : NormedAddCommGroup E] {s : Set Y} [inst_3 : CompactSpace ↑s] (f : X → Y → E) (g : C(↑s, E)),
  (∀ᵐ (x : X) ∂μ, ContinuousOn (f x) s) →
    ∀ (bound : X → ℝ),
      MeasureTheory.HasFiniteIntegral bound μ →
        (∀ᵐ (x : X) ∂μ, ∀ y ∈ s, ‖f x y‖ ≤ bound x) →
          MeasureTheory.HasFiniteIntegral (fun x => ContinuousMap.mkD (s.domRestrict (f x)) g) μ
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.Measure.eq_zero_of_isEmpty : ∀ {α : Type u_1} [IsEmpty α] {_m : MeasurableSpace α} (μ : MeasureTheory.Measure α), μ = 0
-- Mathlib.Order.Filter.Map
Filter.comap_equiv_symm : ∀ {α : Type u_1} {β : Type u_2} (e : α ≃ β) (f : Filter α), Filter.comap (⇑e.symm) f = Filter.map (⇑e) f
-- Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra
Module.FaithfullyFlat.of_isIntegral_of_isDomain : ∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] [IsDomain B]
  [Module.Flat A B] [Algebra.IsIntegral A B] [FaithfulSMul A B], Module.FaithfullyFlat A B
-- Std.Data.DTreeMap.Basic
Std.DTreeMap.instLawfulSingletonSigma : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering}, LawfulSingleton ((a : α) × β a) (Std.DTreeMap α β cmp)
-- Mathlib.Analysis.RCLike.Basic
RCLike.realRingEquiv_symm_apply : ∀ {K : Type u_1} [inst : RCLike K] (h : RCLike.I = 0) (a : ℝ), (RCLike.realRingEquiv h).symm a = ↑a
-- Init.Data.String.Basic
String.utf8ByteSize_push : ∀ {s : String} {c : Char}, (s.push c).utf8ByteSize = s.utf8ByteSize + c.utf8Size
-- Lean.Expr
/-- Like `Lean.Expr.getAppFn` but assumes the application has up to `maxArgs` arguments.
If there are any more arguments than this, then they are returned by `getAppFn` as part of the function.

In particular, if the given expression is a sequence of function applications `f a₁ .. aₙ`,
returns `f a₁ .. aₖ` where `k` is minimal such that `n - k ≤ maxArgs`.
 -/
Lean.Expr.getBoundedAppFn : ℕ → Lean.Expr → Lean.Expr
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Power.revlex : Lean.Grind.CommRing.Power → Lean.Grind.CommRing.Power → Ordering
-- Mathlib.Tactic.CongrExclamation
/-- A list of all the congruence strategies used by `Lean.MVarId.congrCore!`.
 -/
Lean.MVarId.congrPasses! : List (String × (Congr!.Config → Lean.MVarId → Lean.MetaM (Option (List Lean.MVarId))))
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
/-- The generic case of the first cosimplicial identity  -/
CategoryTheory.CosimplicialObject.δ_comp_δ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject C) {n : ℕ}
  {i j : Fin (n + 2)},
  i ≤ j →
    CategoryTheory.CategoryStruct.comp (X.δ i) (X.δ j.succ) =
      CategoryTheory.CategoryStruct.comp (X.δ j) (X.δ i.castSucc)
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.MemLp.congr_enorm : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} {ε : Type u_7} {ε' : Type u_8}
  [inst : TopologicalSpace ε] [inst_1 : TopologicalSpace ε'] [inst_2 : ContinuousENorm ε] [inst_3 : ContinuousENorm ε']
  {f : α → ε} {g : α → ε'},
  MeasureTheory.MemLp f p μ →
    MeasureTheory.AEStronglyMeasurable g μ → (∀ᵐ (a : α) ∂μ, ‖f a‖ₑ = ‖g a‖ₑ) → MeasureTheory.MemLp g p μ
-- Mathlib.Analysis.Normed.Group.Hom
NormedAddGroupHom.ker_zero : ∀ {V₁ : Type u_3} {V₂ : Type u_4} [inst : SeminormedAddCommGroup V₁] [inst_1 : SeminormedAddCommGroup V₂],
  NormedAddGroupHom.ker 0 = ⊤
-- Mathlib.Algebra.Group.Hom.Defs
map_comp_one : ∀ {ι : Type u_1} {M : Type u_4} {N : Type u_5} {F : Type u_9} [inst : One M] [inst_1 : One N] [inst_2 : FunLike F M N]
  [OneHomClass F M N] (f : F), ⇑f ∘ 1 = 1
-- Init.Grind.Ring.Basic
Lean.Grind.Ring.intCast_nat_add : ∀ {α : Type u} [inst : Lean.Grind.Ring α] {x y : ℕ}, ↑(↑x + ↑y) = ↑x + ↑y
-- Mathlib.Geometry.Euclidean.Circumcenter
/-- The center of the circumsphere is the circumcenter.  -/
Affine.Simplex.circumsphere_center : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P n), s.circumsphere.center = s.circumcenter
-- Mathlib.Algebra.DirectSum.Module
DirectSum.instSMulCommClass : ∀ {R : Type u} [inst : Semiring R] {ι : Type v} {M : ι → Type w} [inst_1 : (i : ι) → AddCommMonoid (M i)]
  [inst_2 : (i : ι) → Module R (M i)] {S : Type u_1} [inst_3 : Semiring S] [inst_4 : (i : ι) → Module S (M i)]
  [∀ (i : ι), SMulCommClass R S (M i)], SMulCommClass R S (DirectSum ι fun i => M i)
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.singleton_isCocircuit : ∀ {α : Type u_1} {M : Matroid α} {e : α}, M.IsCocircuit {e} ↔ M.IsColoop e
-- Mathlib.RingTheory.QuasiFinite.Basic
Algebra.QuasiFinite.finite_comap_preimage : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [Algebra.QuasiFinite R S] {s : Set (PrimeSpectrum R)}, s.Finite → (PrimeSpectrum.comap (algebraMap R S) ⁻¹' s).Finite
-- Mathlib.Data.List.Basic
List.mem_map_of_injective : ∀ {α : Type u} {β : Type v} {f : α → β}, Function.Injective f → ∀ {a : α} {l : List α}, f a ∈ List.map f l ↔ a ∈ l
-- Mathlib.NumberTheory.HeckeRing.Defs
/-- The sanctioned constructor of `HeckeCosetModule Δ H₁ H₂ Z` from a finitely-supported function
on double cosets. Build elements through `of` rather than relying on the definitional unfolding
`HeckeCosetModule Δ H₁ H₂ Z = (HeckeCoset Δ H₁ H₂ →₀ Z)`.  -/
HeckeCosetModule.of : {G : Type u_1} →
  [inst : Group G] →
    {Δ : Submonoid G} →
      {H₁ H₂ : Subgroup G} → {Z : Type u_3} → [inst_1 : Zero Z] → (HeckeCoset Δ H₁ H₂ →₀ Z) ≃ HeckeCosetModule Δ H₁ H₂ Z
-- Std.Data.HashSet.Lemmas
Std.HashSet.forIn_eq_forIn_toArray : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} {δ : Type v} {m' : Type v → Type w} [inst : Monad m']
  [LawfulMonad m'] {f : α → δ → m' (ForInStep δ)} {init : δ},
  Std.HashSet.forIn (fun a d => f a d) init m = forIn m.toArray init f
-- Mathlib.RingTheory.Polynomial.DegreeLT
Polynomial.det_taylorLinearEquiv_toLinearMap : ∀ {R : Type u_1} [inst : CommRing R] {r : R} {n : ℕ}, LinearMap.det ↑(Polynomial.taylorLinearEquiv r n) = 1
-- Mathlib.Tactic.Linter.UnusedInstancesInType
/-- Gets the indices `i` (in ascending order) of the binders of a nested `.forallE`,
`(x₀ : A₀) → (x₁ : A₁) → ⋯ → X`, such that
- the binder `[xᵢ : Aᵢ]` has `instImplicit` `binderInfo`
-  `p Aᵢ` is `true`
- The rest of the type `(xᵢ₊₁ : Aᵢ₊₁) → ⋯ → X` does not depend on `xᵢ` outside of proofs.

This is like `getForallUnusedInstanceBinderIdxsWhere`, but ignores dependence that arises from
within proof terms.

The indices start at 0, and do not count `let`s.
 -/
_private.Mathlib.Tactic.Linter.UnusedInstancesInType.0.Lean.Expr.collectUnnecessaryInstanceBinderIdxsWhere : (Lean.Expr → Bool) → Lean.Expr → Lean.MetaM (Array ℕ)