mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Seq.Computation
_private.Mathlib.Data.Seq.Computation.0.Computation.LiftRelAux.match_1.eq_3 : ∀ {α : Type u_1} {β : Type u_2} (motive : α ⊕ Computation α → β ⊕ Computation β → Sort u_3) (ca : Computation α) (b : β)
  (h_1 : (a : α) → (b : β) → motive (Sum.inl a) (Sum.inl b))
  (h_2 : (a : α) → (cb : Computation β) → motive (Sum.inl a) (Sum.inr cb))
  (h_3 : (ca : Computation α) → (b : β) → motive (Sum.inr ca) (Sum.inl b))
  (h_4 : (ca : Computation α) → (cb : Computation β) → motive (Sum.inr ca) (Sum.inr cb)),
  (match Sum.inr ca, Sum.inl b with
    | Sum.inl a, Sum.inl b => h_1 a b
    | Sum.inl a, Sum.inr cb => h_2 a cb
    | Sum.inr ca, Sum.inl b => h_3 ca b
    | Sum.inr ca, Sum.inr cb => h_4 ca cb) =
    h_3 ca b
-- Init.Control.Lawful.Instances
Option.elim.eq_2 : ∀ {α : Type u_1} {β : Sort u_2} (x : β) (x_1 : α → β), none.elim x x_1 = x
-- Lean.Elab.Tactic.Basic
_private.Lean.Elab.Tactic.Basic.0.Lean.Elab.Tactic.TacticM.runCore : {α : Type} →
  Lean.Elab.Tactic.TacticM α →
    Lean.Elab.Tactic.Context → Lean.Elab.Tactic.State → Lean.Elab.TermElabM (α × Lean.Elab.Tactic.State)
-- Std.Http.Data.Response
Std.Http.Response.mk : {t : Type} → Std.Http.Response.Head → t → Std.Http.Extensions → Std.Http.Response t
-- Mathlib.CategoryTheory.Category.Basic
CategoryTheory.mono_of_mono_fac : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : Y ⟶ X} {g : Z ⟶ Y} {h : Z ⟶ X}
  [CategoryTheory.Mono h], CategoryTheory.CategoryStruct.comp g f = h → CategoryTheory.Mono g
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey!_diff_of_mem_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtDTreeMap α β cmp} [inst : Inhabited α]
  [inst_1 : Std.TransCmp cmp] {k : α}, k ∈ t₂ → (t₁ \ t₂).getKey! k = default
-- Lean.ScopedEnvExtension
Lean.ScopedEnvExtension : Type → Type → Type → Type
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.Equiv.getKey_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {hk : k ∈ t₁} (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂), t₁.getKey k hk = t₂.getKey k ⋯
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Expr.toPoly.match_4.congr_eq_3 : ∀ (motive : Lean.Grind.CommRing.Expr → Sort u_1) (x : Lean.Grind.CommRing.Expr)
  (h_1 : (k : ℤ) → motive (Lean.Grind.CommRing.Expr.num k))
  (h_2 : (k : ℤ) → motive (Lean.Grind.CommRing.Expr.intCast k))
  (h_3 : (k : ℕ) → motive (Lean.Grind.CommRing.Expr.natCast k))
  (h_4 : (x : Lean.Grind.CommRing.Var) → motive (Lean.Grind.CommRing.Expr.var x))
  (h_5 : (a b : Lean.Grind.CommRing.Expr) → motive (a.add b))
  (h_6 : (a b : Lean.Grind.CommRing.Expr) → motive (a.mul b)) (h_7 : (a : Lean.Grind.CommRing.Expr) → motive a.neg)
  (h_8 : (a b : Lean.Grind.CommRing.Expr) → motive (a.sub b))
  (h_9 : (a : Lean.Grind.CommRing.Expr) → (k : ℕ) → motive (a.pow k)) (k : ℕ),
  x = Lean.Grind.CommRing.Expr.natCast k →
    (match x with
      | Lean.Grind.CommRing.Expr.num k => h_1 k
      | Lean.Grind.CommRing.Expr.intCast k => h_2 k
      | Lean.Grind.CommRing.Expr.natCast k => h_3 k
      | Lean.Grind.CommRing.Expr.var x => h_4 x
      | a.add b => h_5 a b
      | a.mul b => h_6 a b
      | a.neg => h_7 a
      | a.sub b => h_8 a b
      | a.pow k => h_9 a k) ≍
      h_3 k
-- Std.Tactic.Do.Syntax
Lean.Parser.Tactic.«mintroPat∀_» : Lean.ParserDescr
-- Mathlib.Order.WellFounded
/-- A nonempty linear order with well-founded `<` has a bottom element.  -/
WellFoundedLT.toOrderBot : (α : Type u_4) → [inst : LinearOrder α] → [Nonempty α] → [h : WellFoundedLT α] → OrderBot α
-- Mathlib.Analysis.Distribution.TemperedDistribution
/-- The canonical embedding of `𝓢(E, F)` into `𝓢'(E, F)` as a continuous linear map.  -/
SchwartzMap.toTemperedDistributionCLM : (E : Type u_3) →
  (F : Type u_4) →
    [inst : NormedAddCommGroup E] →
      [inst_1 : NormedSpace ℝ E] →
        [inst_2 : NormedAddCommGroup F] →
          [inst_3 : NormedSpace ℂ F] →
            [inst_4 : MeasurableSpace E] →
              [BorelSpace E] →
                [SecondCountableTopology E] →
                  (μ : autoParam (MeasureTheory.Measure E) SchwartzMap.toTemperedDistributionCLM._auto_1) →
                    [hμ : μ.HasTemperateGrowth] → SchwartzMap E F →L[ℂ] TemperedDistribution E F
-- Mathlib.Order.GaloisConnection.Basic
GaloisConnection.l_sSup : ∀ {α : Type u} {β : Type v} [inst : CompleteLattice α] [inst_1 : CompleteLattice β] {l : α → β} {u : β → α},
  GaloisConnection l u → ∀ {s : Set α}, l (sSup s) = ⨆ a ∈ s, l a
-- Std.Http.Data.URI.Parser
_private.Std.Http.Data.URI.Parser.0.Std.Http.URI.Parser.tryOpt : {α : Type} → Std.Internal.Parsec.ByteArray.Parser α → Std.Internal.Parsec.ByteArray.Parser (Option α)
-- Init.Data.UInt.Lemmas
USize.mod_lt : ∀ (a : USize) {b : USize}, 0 < b → a % b < b
-- Mathlib.Data.Finset.Prod
Finset.subset_product_image_fst : ∀ {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} [inst : DecidableEq α], Finset.image Prod.fst (s ×ˢ t) ⊆ s
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrp.forget₂AddMon_obj_add : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (A : CategoryTheory.AddGrp C), CategoryTheory.AddMonObj.add = CategoryTheory.AddMonObj.add
-- Mathlib.Algebra.Order.Ring.Abs
abs_dvd_self : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : LinearOrder α] (a : α), |a| ∣ a
-- Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar
MeasureTheory.addEquivAddHaarChar_eq_one_of_compactSpace : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [inst_2 : MeasurableSpace G] [inst_3 : BorelSpace G]
  [inst_4 : IsTopologicalAddGroup G] [inst_5 : LocallyCompactSpace G] [CompactSpace G] (φ : G ≃ₜ+ G),
  MeasureTheory.addEquivAddHaarChar φ = 1
-- Mathlib.Algebra.Module.Congruence.Defs
/-- The `AddCon` generated by a `SMulCon` is a `ModuleCon`.  -/
SMulCon.addConGen : {S : Type u_2} → {M : Type u_3} → [inst : AddZeroClass M] → [inst_1 : DistribSMul S M] → SMulCon S M → ModuleCon S M
-- Mathlib.CategoryTheory.MorphismProperty.LocalClosure
CategoryTheory.MorphismProperty.sourceLocalClosure.below.of : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {K : CategoryTheory.Precoverage C}
  {P : CategoryTheory.MorphismProperty C}
  {motive : ⦃X Y : C⦄ → (x : X ⟶ Y) → CategoryTheory.MorphismProperty.sourceLocalClosure K P x → Prop} {X Y : C}
  (f : X ⟶ Y) (a : P f), CategoryTheory.MorphismProperty.sourceLocalClosure.below ⋯
-- Mathlib.Algebra.Symmetrized
SymAlg.instInvertibleCoeEquivSym : {α : Type u_1} →
  [inst : Mul α] →
    [inst_1 : AddMonoidWithOne α] → [inst_2 : Invertible 2] → (a : α) → [Invertible a] → Invertible (SymAlg.sym a)
-- Mathlib.RingTheory.Polynomial.Pochhammer
descPochhammer.eq_2 : ∀ (R : Type u) [inst : Ring R] (n : ℕ),
  descPochhammer R n.succ = Polynomial.X * (descPochhammer R n).comp (Polynomial.X - 1)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.minKey?_alter_eq_self : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {k : α} {f : Option β → Option β},
  (Std.ExtDTreeMap.Const.alter t k f).minKey? = some k ↔
    (f (Std.ExtDTreeMap.Const.get? t k)).isSome = true ∧ ∀ k' ∈ t, (cmp k k').isLE = true
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.union_eq : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m₁ m₂ : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α], m₁.union m₂ = m₁ ∪ m₂
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.coeff_single_mul_aux : ∀ {k : Type u_1} {G : Type u_2} [inst : Semiring k] [inst_1 : Mul G] [inst_2 : SMulZeroClass G k]
  (f : SkewMonoidAlgebra k G) {r : k} {x y z : G},
  (∀ (a : G), x * a = y ↔ a = z) → (SkewMonoidAlgebra.single x r * f).coeff y = r * x • f.coeff z
-- Mathlib.Order.SuccPred.Limit
Order.IsSuccLimit.subtypeVal : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α}, IsLowerSet s → ∀ {a : ↑s}, Order.IsSuccLimit a → Order.IsSuccLimit ↑a
-- Mathlib.RingTheory.Localization.BaseChange
IsLocalization.instCompatibleSMulLocalizationOfIsScalarTower_1 : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) (M₁ : Type u_5) (M₂ : Type u_6) [inst_1 : AddCommMonoid M₁]
  [inst_2 : AddCommMonoid M₂] [inst_3 : Module R M₁] [inst_4 : Module R M₂] [inst_5 : Module (Localization S) M₁]
  [inst_6 : Module (Localization S) M₂] [IsScalarTower R (Localization S) M₁] [IsScalarTower R (Localization S) M₂],
  TensorProduct.CompatibleSMul R (Localization S) M₁ M₂
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.get?_eq_some_getD_of_contains : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α],
  m.WF → ∀ {a : α} {fallback : β a}, m.contains a = true → m.get? a = some (m.getD a fallback)
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.isEmpty_inter_iff : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α], (m₁ ∩ m₂).isEmpty = true ↔ ∀ k ∈ m₁, k ∉ m₂
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.isSome_minKey?_of_isSome_minKey?_erase : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α},
  (t.erase k).minKey?.isSome = true → t.minKey?.isSome = true
-- Mathlib.Data.ZMod.Basic
ZMod.natCast_eq_iff : ∀ (p n : ℕ) (z : ZMod p) [NeZero p], ↑n = z ↔ ∃ k, n = z.val + p * k
-- Mathlib.Algebra.Ring.Action.Basic
MulSemiringAction.toMulDistribMulAction : (M : Type u_3) →
  (R : Type u_4) → {x : Monoid M} → {x_1 : Semiring R} → [h : MulSemiringAction M R] → MulDistribMulAction M R
-- Mathlib.Data.Sym.Sym2
/-- The symmetric square is equivalent to length-2 vectors up to permutations.  -/
Sym2.sym2EquivSym' : {α : Type u_1} → Sym2 α ≃ Sym.Sym' α 2
-- Mathlib.GroupTheory.Congruence.Defs
AddCon.hrec_on₂_coe : ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] {cM : AddCon M} {cN : AddCon N}
  {φ : cM.Quotient → cN.Quotient → Sort u_4} (a : M) (b : N) (f : (x : M) → (y : N) → φ ↑x ↑y)
  (h : ∀ (x : M) (y : N) (x' : M) (y' : N), cM x x' → cN y y' → f x y ≍ f x' y'), AddCon.hrecOn₂ (↑a) (↑b) f h = f a b
-- Mathlib.Analysis.InnerProductSpace.PiL2
OrthonormalBasis.singleton_apply : ∀ {ι : Type u_7} {𝕜 : Type u_8} [inst : Unique ι] [inst_1 : RCLike 𝕜] (i : ι), (OrthonormalBasis.singleton ι 𝕜) i = 1
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.mem_carrier : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] {s : IntermediateField K L}
  {x : L}, x ∈ s.carrier ↔ x ∈ s
-- Lean.MetavarContext
/-- `LocalInstance` represents a local typeclass instance registered by and for
the elaborator. It stores the name of the typeclass in `className`, and the
concrete typeclass instance in `fvar`. Note that the kernel does not care about
this information, since typeclasses are entirely eliminated during elaboration.
 -/
Lean.LocalInstance : Type
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
le_of_forall_one_lt_lt_mul : ∀ {α : Type u} [inst : Group α] [inst_1 : LinearOrder α] [MulLeftMono α] {a b : α},
  (∀ (ε : α), 1 < ε → a < b * ε) → a ≤ b
-- Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Polynomial.eval₂_one_cyclotomic_prime_pow : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : Semiring S] (f : R →+* S) {p : ℕ} (k : ℕ)
  [Fact (Nat.Prime p)], Polynomial.eval₂ f 1 (Polynomial.cyclotomic (p ^ (k + 1)) R) = ↑p
-- Aesop.Search.Expansion.Simp
Aesop.SimpResult.solved.sizeOf_spec : ∀ (usedTheorems : Lean.Meta.Simp.UsedSimps), sizeOf (Aesop.SimpResult.solved usedTheorems) = 1 + sizeOf usedTheorems
-- Lean.Expr
Lean.MVarId.mk.injEq : ∀ (name name_1 : Lean.Name), ({ name := name } = { name := name_1 }) = (name = name_1)
-- Mathlib.CategoryTheory.Monad.Adjunction
/-- The adjunction `monadicLeftAdjoint R ⊣ R` given by `[MonadicRightAdjoint R]`.  -/
CategoryTheory.monadicAdjunction : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (R : CategoryTheory.Functor D C) →
          [inst_2 : CategoryTheory.MonadicRightAdjoint R] → CategoryTheory.monadicLeftAdjoint R ⊣ R
-- Mathlib.Algebra.Module.NatInt
/-- All `ℕ`-module structures are equal. Not an instance since in mathlib all `AddCommMonoid`
should normally have exactly one `ℕ`-module structure by design.  -/
AddCommMonoid.uniqueNatModule : {M : Type u_3} → [inst : AddCommMonoid M] → Unique (Module ℕ M)
-- Lean.Language.Lean.Types
/-- The resulting initial elaboration state.  -/
Lean.Language.Lean.HeaderProcessedState.cmdState : Lean.Language.Lean.HeaderProcessedState → Lean.Elab.Command.State
-- Mathlib.Algebra.Polynomial.Laurent
LaurentPolynomial.smeval_zero : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid S] [inst_2 : SMulWithZero R S]
  [inst_3 : Monoid S] (x : Sˣ), LaurentPolynomial.smeval 0 x = 0
-- Std.Data.ExtTreeSet.Basic
/-- Returns `true` if the tree set contains no mappings.  -/
Std.ExtTreeSet.isEmpty : {α : Type u} → {cmp : α → α → Ordering} → Std.ExtTreeSet α cmp → Bool
-- Init.Data.List.Nat.Count
List.count_replace : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {a b c : α} {l : List α},
  List.count c (l.replace a b) =
    if l.contains a = true then (List.count c l + if (b == c) = true then 1 else 0) - if (a == c) = true then 1 else 0
    else List.count c l
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.inclusion.eq_1 : ∀ {M : Type u_1} [inst : AddZeroClass M] {S T : AddSubmonoid M} (h : S ≤ T),
  AddSubmonoid.inclusion h = S.subtype.codRestrict T ⋯
-- Mathlib.Topology.MetricSpace.Ultra.Basic
IsUltrametricDist.isClopen_ball : ∀ {X : Type u_1} [inst : PseudoMetricSpace X] [IsUltrametricDist X] (x : X) (r : ℝ), IsClopen (Metric.ball x r)
-- Init.Data.List.Nat.Modify
List.getElem?_modify_ne : ∀ {α : Type u_1} (f : α → α) {i j : ℕ} (l : List α), i ≠ j → (l.modify i f)[j]? = l[j]?
-- Mathlib.Computability.Partrec
Nat.Partrec.pair : ∀ {f g : ℕ →. ℕ}, Nat.Partrec f → Nat.Partrec g → Nat.Partrec fun n => Nat.pair <$> f n <*> g n
-- Mathlib.Order.Category.Frm
/-- Constructs an isomorphism of frames from an order isomorphism between them.  -/
Frm.Iso.mk : {α β : Frm} → ↑α ≃o ↑β → (α ≅ β)
-- Mathlib.MeasureTheory.Function.Floor
Nat.measurable_floor : ∀ {R : Type u_2} [inst : Semiring R] [inst_1 : LinearOrder R] [inst_2 : FloorSemiring R] [inst_3 : TopologicalSpace R]
  [OrderTopology R] [inst_5 : MeasurableSpace R] [OpensMeasurableSpace R] [IsStrictOrderedRing R], Measurable Nat.floor
-- Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
/-- The `ℝ`-valued sequence sending `n` to `(μ (x ^ n))^(1/n : ℝ)`.  -/
smoothingSeminormSeq : {R : Type u_1} → [inst : CommRing R] → RingSeminorm R → R → ℕ → ℝ
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.isEmpty.congr_simp : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  (m m_1 : Std.ExtDHashMap α β), m = m_1 → m.isEmpty = m_1.isEmpty
-- Mathlib.Algebra.Order.Ring.Canonical
Odd.pos : ∀ {R : Type u} [inst : Semiring R] [inst_1 : PartialOrder R] [CanonicallyOrderedAdd R] [Nontrivial R] {a : R},
  Odd a → 0 < a
-- Mathlib.Algebra.Order.Group.Lattice
neg_inf : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : AddGroup α] [AddLeftMono α] [AddRightMono α] (a b : α), -(a ⊓ b) = -a ⊔ -b
-- Mathlib.NumberTheory.Padics.RingHoms
PadicInt.modPart_lt_p : ∀ {p : ℕ} [hp_prime : Fact (Nat.Prime p)] (r : ℚ), PadicInt.modPart p r < ↑p
-- Lean.Meta.Tactic.FVarSubst
/-- Add entry `fvarId |-> v` to `s` if `s` does not contain an entry for `fvarId`.  -/
Lean.Meta.FVarSubst.insert : Lean.Meta.FVarSubst → Lean.FVarId → Lean.Expr → Lean.Meta.FVarSubst
-- Init.System.IO
/-- Creates a new task that waits for `t` to complete and then runs the `BaseIO` action `f` on its
result. This new task has priority `prio`.

Running the resulting `BaseIO` action causes the task to be started eagerly. Unlike pure tasks
created by `Task.spawn`, tasks created by this function will run even if the last reference to the
task is dropped. The `act` should explicitly check for cancellation via `IO.checkCanceled` if it
should be terminated or otherwise react to the last reference being dropped.
 -/
BaseIO.mapTask : {α : Type u_1} →
  {β : Type} →
    (α → BaseIO β) → Task α → optParam Task.Priority Task.Priority.default → optParam Bool false → BaseIO (Task β)
-- Mathlib.Analysis.SpecialFunctions.Integrability.Basic
/-- See `intervalIntegrable_rpow` for a version applying to any locally finite measure, but with a
stronger hypothesis on `r`.  -/
intervalIntegral.intervalIntegrable_rpow' : ∀ {a b r : ℝ}, -1 < r → IntervalIntegrable (fun x => x ^ r) MeasureTheory.volume a b
-- Init.Data.SInt.Lemmas
Int64.toInt_ofInt : ∀ {n : ℤ}, (Int64.ofInt n).toInt = n.bmod Int64.size
-- Init.Prelude
/-- The array of elements and separators, ordered like
`#[el1, sep1, el2, sep2, el3]`.  -/
Lean.Syntax.TSepArray.elemsAndSeps : {ks : Lean.SyntaxNodeKinds} → {sep : String} → Lean.Syntax.TSepArray ks sep → Array Lean.Syntax
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
CategoryTheory.Functor.is_cover_of_isCoverDense : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (G : CategoryTheory.Functor C D)
  (K : CategoryTheory.GrothendieckTopology D) [G.IsCoverDense K] (U : D), CategoryTheory.Sieve.coverByImage G U ∈ K U
-- Mathlib.Order.Notation
Top.mk : {α : Type u_1} → α → Top α
-- Mathlib.Analysis.Complex.Polynomial.GaussLucas
Polynomial.derivRootWeight_nonneg : ∀ (P : Polynomial ℂ) (z w : ℂ), 0 ≤ P.derivRootWeight z w
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.minKey_insertIfNew_of_isEmpty : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β}, t.isEmpty = true → (t.insertIfNew k v).minKey ⋯ = k
-- Mathlib.Algebra.Order.Monoid.Unbundled.TypeTags
Additive.toMul_eq_bot : ∀ {α : Type u_1} [inst : LE α] [inst_1 : OrderBot α] {a : Additive α}, Additive.toMul a = ⊥ ↔ a = ⊥
-- Mathlib.Analysis.Distribution.Sobolev
TemperedDistribution.besselPotential_neg_apply_eq_iff : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F]
  [inst_2 : InnerProductSpace ℝ E] [inst_3 : FiniteDimensional ℝ E] [inst_4 : MeasurableSpace E] [inst_5 : BorelSpace E]
  [inst_6 : NormedSpace ℂ F] (s : ℝ) (f g : TemperedDistribution E F),
  (TemperedDistribution.besselPotential E F (-s)) f = g ↔ (TemperedDistribution.besselPotential E F s) g = f
-- Mathlib.Algebra.Group.Shrink
equivShrink_symm_inv : ∀ {α : Type u_2} [inst : Small.{v, u_2} α] [inst_1 : Inv α] (x : Shrink.{v, u_2} α),
  (equivShrink α).symm x⁻¹ = ((equivShrink α).symm x)⁻¹
-- Mathlib.Algebra.Group.Basic
inv_involutive : ∀ {G : Type u_3} [inst : InvolutiveInv G], Function.Involutive Inv.inv
-- Mathlib.Analysis.Meromorphic.Basic
MeromorphicAt.pow : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {x : 𝕜} {f : 𝕜 → 𝕜'}, MeromorphicAt f x → ∀ (n : ℕ), MeromorphicAt (f ^ n) x
-- Mathlib.Order.OrderIsoNat
exists_increasing_or_nonincreasing_subseq' : ∀ {α : Type u_1} (r : α → α → Prop) (f : ℕ → α),
  ∃ g, (∀ (n : ℕ), r (f (g n)) (f (g (n + 1)))) ∨ ∀ (m n : ℕ), m < n → ¬r (f (g m)) (f (g n))
-- Aesop.Frontend.Extension
Aesop.Frontend.modifyGlobalRuleSet : Aesop.RuleSetName → (Aesop.GlobalRuleSet → Aesop.GlobalRuleSet) → Lean.CoreM Unit
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
/-- **Alias** of `NonUnitalAlgebra.toNonUnitalSubring_eq_top`. -/
NonUnitalAlgebra.to_subring_eq_top : ∀ {R : Type u_2} {A : Type u_3} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A]
  {S : NonUnitalSubalgebra R A}, S.toNonUnitalSubring = ⊤ ↔ S = ⊤
-- Init.Data.SInt.Bitwise
instCommutativeInt64HOr : Std.Commutative fun x1 x2 => x1 ||| x2
-- Lean.Meta.Tactic.Grind.EMatchTheorem
/-- `detectOffsets` inverse.
This function is used to expand `mkOffsetPattern` occurring in a constant pattern.
 -/
_private.Lean.Meta.Tactic.Grind.EMatchTheorem.0.Lean.Meta.Grind.expandOffsetPatterns : Lean.Expr → Lean.CoreM Lean.Expr
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
/-- The set of nonnegative elements in a C⋆-algebra is closed.  -/
CStarAlgebra.isClosed_nonneg : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] [StarOrderedRing A], IsClosed {a | 0 ≤ a}
-- Mathlib.Computability.TuringMachine.Tape
Turing.instDecidableEqDir : DecidableEq Turing.Dir
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey!_insertIfNew : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  [inst : Inhabited α] {k a : α} {v : β},
  (m.insertIfNew k v).getKey! a = if (k == a) = true ∧ k ∉ m then k else m.getKey! a
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.δ_ofHomotopy : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} {φ₁ φ₂ : F ⟶ G} (h : Homotopy φ₁ φ₂),
  CochainComplex.HomComplex.δ (-1) 0 (CochainComplex.HomComplex.Cochain.ofHomotopy h) =
    CochainComplex.HomComplex.Cochain.ofHom φ₁ - CochainComplex.HomComplex.Cochain.ofHom φ₂
-- Lean.Meta.Match.CaseValues
/-- Split goal `... |- C x`,, where `fvarId` is `x`s id, into two subgoals
`..., |- (h : x = value)  → C x`
`..., |- (h : x != value) → C x`
The type of `x` must have decidable equality.
 -/
_private.Lean.Meta.Match.CaseValues.0.Lean.Meta.caseValue : Lean.MVarId → Lean.FVarId → Lean.Expr → optParam Lean.Name `h → Lean.MetaM (Lean.MVarId × Lean.MVarId)
-- Init.Data.BitVec.Lemmas
BitVec.fill_toInt : ∀ {w : ℕ} {v : Bool}, (BitVec.fill w v).toInt = if (decide (v = true) && decide (0 < w)) = true then -1 else 0
-- Mathlib.Algebra.BigOperators.Fin
Fin.sum_Iic_cast : ∀ {M : Type u_2} [inst : AddCommMonoid M] {n m : ℕ} (h : n = m) (f : Fin m → M) (a : Fin n),
  ∑ i ≤ Fin.cast h a, f i = ∑ i ≤ a, f (Fin.cast h i)
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.inv_apply : ∀ {ι : Type u_1} (R : ι → Type u_2) {𝓕 : Filter ι} {S : ι → Type u_3} [inst : (i : ι) → SetLike (S i) (R i)]
  {B : (i : ι) → S i} [inst_1 : (i : ι) → Inv (R i)] [inst_2 : ∀ (i : ι), InvMemClass (S i) (R i)]
  (x : RestrictedProduct (fun i => R i) (fun i => ↑(B i)) 𝓕) (i : ι), x⁻¹ i = (x i)⁻¹
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
/-- This enables the notation `⨂[R] i : ι, s i` for the pi tensor product `PiTensorProduct`,
given an indexed family of types `s : ι → Type*`.  -/
TensorProduct.«term⨂[_]_,_» : Lean.ParserDescr
-- Mathlib.Topology.Category.LightProfinite.Extend
/-- `S.asLimitCone'` is a limit cone.  -/
LightProfinite.asLimit' : (S : LightProfinite) → CategoryTheory.Limits.IsLimit S.asLimitCone'
-- Mathlib.Geometry.Manifold.ContMDiff.Constructions
contMDiff_prod_module_iff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F₁ : Type u_14} [inst_6 : NormedAddCommGroup F₁]
  [inst_7 : NormedSpace 𝕜 F₁] {F₂ : Type u_15} [inst_8 : NormedAddCommGroup F₂] [inst_9 : NormedSpace 𝕜 F₂]
  {n : WithTop ℕ∞} (f : M → F₁ × F₂),
  ContMDiff I (modelWithCornersSelf 𝕜 (F₁ × F₂)) n f ↔
    ContMDiff I (modelWithCornersSelf 𝕜 F₁) n (Prod.fst ∘ f) ∧ ContMDiff I (modelWithCornersSelf 𝕜 F₂) n (Prod.snd ∘ f)
-- Mathlib.RingTheory.DividedPowers.RatAlgebra
DividedPowers.IsNilpotent.dpow_of_prime_le : ∀ {A : Type u_1} [inst : CommRing A] {p : ℕ} [inst_1 : Fact (Nat.Prime p)] (hp : IsNilpotent ↑p) {I : Ideal A}
  [inst_2 : DecidablePred fun x => x ∈ I] (hIp : I ^ p = 0) {n : ℕ},
  p ≤ n → ∀ (a : A), (DividedPowers.IsNilpotent.dividedPowers hp hIp).dpow n a = 0
-- Mathlib.Order.Filter.SmallSets
Filter.smallSets_top : ∀ {α : Type u_1}, ⊤.smallSets = ⊤
-- Mathlib.Combinatorics.SimpleGraph.Walk.Counting
SimpleGraph.fintypeSetWalkLength : {V : Type u} →
  (G : SimpleGraph V) → [DecidableEq V] → [G.LocallyFinite] → (u v : V) → (n : ℕ) → Fintype ↑{p | p.length = n}