mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RepresentationTheory.FiniteIndex
/-- Given a finite index subgroup `S ≤ G`, `Ind_S^G` is right adjoint to the restriction functor
`Res k G ⥤ Res k S`, since it is naturally isomorphic to `Coind_S^G`.  -/
Rep.resIndAdjunction : (k : Type u) →
  {G : Type v} →
    [inst : CommRing k] →
      [inst_1 : Group G] →
        (S : Subgroup G) →
          [DecidableRel ⇑(QuotientGroup.rightRel S)] →
            [S.FiniteIndex] → Rep.resFunctor S.subtype ⊣ Rep.indFunctor k S.subtype
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey_getValue?_ext : ∀ {α : Type u} [inst : BEq α] [EquivBEq α] {β : Type v} {l l' : List ((_ : α) × β)},
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.DistinctKeys l' →
      (∀ (a : α) (h : Std.Internal.List.containsKey a l = true) (h' : Std.Internal.List.containsKey a l' = true),
          Std.Internal.List.getKey a l h = Std.Internal.List.getKey a l' h') →
        (∀ (a : α), Std.Internal.List.getValue? a l = Std.Internal.List.getValue? a l') → l.Perm l'
-- Mathlib.Order.Filter.Bases.Basic
Filter.HasBasis.ge_iff : ∀ {α : Type u_1} {ι' : Sort u_5} {l l' : Filter α} {p' : ι' → Prop} {s' : ι' → Set α},
  l'.HasBasis p' s' → (l ≤ l' ↔ ∀ (i' : ι'), p' i' → s' i' ∈ l)
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.comp₂_eq_mk : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α}
  [inst_1 : TopologicalSpace δ] [inst_2 : TopologicalSpace β] [inst_3 : TopologicalSpace γ] (g : β → γ → δ)
  (hg : Continuous (Function.uncurry g)) (f₁ : α →ₘ[μ] β) (f₂ : α →ₘ[μ] γ),
  MeasureTheory.AEEqFun.comp₂ g hg f₁ f₂ = MeasureTheory.AEEqFun.mk (fun a => g (↑f₁ a) (↑f₂ a)) ⋯
-- Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
/-- The typeclass saying that `P : ObjectProperty C` is stable under binary products.  -/
CategoryTheory.ObjectProperty.IsClosedUnderBinaryProducts : {C : Type u_1} → [inst : CategoryTheory.Category.{v_1, u_1} C] → CategoryTheory.ObjectProperty C → Prop
-- Mathlib.Algebra.Order.AddGroupWithTop
LinearOrderedAddCommGroupWithTop.add_neg_cancel_right_of_ne_top : ∀ {α : Type u_2} [inst : LinearOrderedAddCommGroupWithTop α] {b : α}, b ≠ ⊤ → ∀ (a : α), a + b + -b = a
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenSubgroup.instMax : {G : Type u_1} → [inst : Group G] → [inst_1 : TopologicalSpace G] → [SeparatelyContinuousMul G] → Max (OpenSubgroup G)
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.tail_think : ∀ {α : Type u} (s : Stream'.WSeq α), s.think.tail = s.tail.think
-- Mathlib.CategoryTheory.Monoidal.CommMon_
CategoryTheory.Functor.mapCommMon_id_mul : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (A : CategoryTheory.CommMon C),
  CategoryTheory.MonObj.mul =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj A.X A.X))
      CategoryTheory.MonObj.mul
-- Init.Data.BitVec.Lemmas
BitVec.toInt_neg_eq_of_msb : ∀ {w : ℕ} {x : BitVec w}, x.msb = false → (-x).toInt = -x.toInt
-- Mathlib.GroupTheory.OreLocalization.Basic
/-- Another characterization lemma for the multiplication on the Ore localization delivering
Ore witnesses and conditions bundled in a sigma type.  -/
OreLocalization.oreDivMulChar' : {R : Type u_1} →
  [inst : Monoid R] →
    {S : Submonoid R} →
      [inst_1 : OreLocalization.OreSet S] →
        (r₁ r₂ : R) →
          (s₁ s₂ : ↥S) → (r' : R) ×' (s' : ↥S) ×' ↑s' * r₁ = r' * ↑s₂ ∧ r₁ /ₒ s₁ * (r₂ /ₒ s₂) = r' * r₂ /ₒ (s' * s₁)
-- Mathlib.Algebra.GroupWithZero.Associated
associates_irreducible_iff_prime : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] [IsCancelMulZero M] [DecompositionMonoid M] {p : Associates M},
  Irreducible p ↔ Prime p
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.coe_singletonOneHom : ∀ {α : Type u_2} [inst : One α], ⇑Finset.singletonOneHom = singleton
-- Mathlib.CategoryTheory.Sites.Coverage
/-- An auxiliary definition used to define the Grothendieck topology associated to a
coverage. See `Coverage.toGrothendieck`.
 -/
CategoryTheory.Coverage.Saturate : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] → CategoryTheory.Coverage C → (X : C) → CategoryTheory.Sieve X → Prop
-- Mathlib.Algebra.Homology.Embedding.RestrictionHomology
HomologicalComplex.pOpcycles_restrictionOpcyclesIso_hom : ∀ {ι : 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 : HomologicalComplex C c') (e : c.Embedding c') [inst_2 : e.IsRelIff] (i j : ι) (hi : c.prev j = i) {i' j' : ι'}
  (hi' : e.f i = i') (hj' : e.f j = j') (hi'' : c'.prev j' = i') [inst_3 : K.HasHomology j']
  [inst_4 : (K.restriction e).HasHomology j],
  CategoryTheory.CategoryStruct.comp ((K.restriction e).pOpcycles j)
      (K.restrictionOpcyclesIso e i j hi hi' hj' hi'').hom =
    CategoryTheory.CategoryStruct.comp (K.restrictionXIso e hj').hom (K.pOpcycles j')
-- Init.Data.Iterators.Combinators.Monadic.Append
/-- This combinator is only useful for advanced use cases.

Given an iterator `it₂`, `IterM.Intermediate.appendSnd α₁ it₂` returns an iterator that behaves
exactly like `it₂` but has the same type as `it₁.append it₂` (after `it₁` has been exhausted).
This is useful for constructing intermediate states of the append iterator.

**Marble diagram:**

```text
it₂                                  --a--b--⊥
IterM.Intermediate.appendSnd α₁ it₂  --a--b--⊥
```

**Termination properties:**

* `Finite` instance: only if `it₂` and iterators of type `α₁` are finite
* `Productive` instance: only if `it₂` and iterators of type `α₁` are productive

Note: If iterators of type `α₁` are not finite, then `appendSnd α₁ it₂` can be productive
while `it₂` is not. The standard library does not provide a `Productive` instance for this case.

**Performance:**

This combinator incurs an additional O(1) cost with each output of `it₂`.
 -/
Std.IterM.Intermediate.appendSnd : {m : Type w → Type w'} → {β α₂ : Type w} → [Std.Iterator α₂ m β] → (α₁ : Type w) → Std.IterM m β → Std.IterM m β
-- Init.Grind.Config
/-- If `matchEqs` is `true`, `grind` uses `match`-equations as E-matching theorems.  -/
Lean.Grind.Config.matchEqs : Lean.Grind.Config → Bool
-- Mathlib.Algebra.Group.TransferInstance
Equiv.mulOneClass.eq_1 : ∀ {α : Type u_2} {β : Type u_3} (e : α ≃ β) [inst : MulOneClass β],
  e.mulOneClass = Function.Injective.mulOneClass ⇑e ⋯ ⋯ ⋯
-- Mathlib.Order.Filter.Defs
Filter.mem_join : ∀ {α : Type u_1} {s : Set α} {f : Filter (Filter α)}, s ∈ f.join ↔ {t | s ∈ t} ∈ f
-- Batteries.Data.UnionFind.Basic
Batteries.UnionFind.FindAux.mk.sizeOf_spec : ∀ {n : ℕ} (s : Array Batteries.UFNode) (root : Fin n) (size_eq : s.size = n),
  sizeOf { s := s, root := root, size_eq := size_eq } = 1 + sizeOf s + sizeOf root + sizeOf size_eq
-- Mathlib.Tactic.Have
/-- Adds hypotheses to the context, turning them into goals to be proved later if their proof terms
aren't provided (`t: Option Term := none`).

If the bound term is intended to be kept in the context, pass `keepTerm : Bool := true`. This is
useful when extending the `let` tactic, which is expected to show the proof term in the infoview.
 -/
Mathlib.Tactic.haveLetCore : Lean.MVarId →
  Lean.TSyntax `Mathlib.Tactic.optBinderIdent →
    Array (Lean.TSyntax `Lean.Parser.Term.letIdBinder) →
      Option Lean.Term → Bool → Lean.Elab.TermElabM (Lean.MVarId × Lean.MVarId)
-- Mathlib.Computability.Primrec.Basic
_private.Mathlib.Computability.Primrec.Basic.0.Encodable.decodeSum.match_1.splitter : (motive : Bool → ℕ → Sort u_1) →
  (x : Bool) →
    (x_1 : ℕ) → ((m : ℕ) → motive false m) → ((x : Bool) → (m : ℕ) → (x = false → False) → motive x m) → motive x x_1
-- Mathlib.Data.Finite.Prod
Finite.instPProd : ∀ {α : Sort u_3} {β : Sort u_4} [Finite α] [Finite β], Finite (α ×' β)
-- Mathlib.Topology.Basic
Filter.lim.eq_1 : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : Nonempty X] (f : Filter X),
  f.lim = Classical.epsilon fun x => f ≤ nhds x
-- Mathlib.FieldTheory.Perfect
Polynomial.roots_expand_image_frobenius : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] {p : ℕ} [inst_2 : ExpChar R p] {f : Polynomial R}
  [PerfectRing R p] [inst_4 : DecidableEq R],
  Finset.image (⇑(frobenius R p)) ((Polynomial.expand R p) f).roots.toFinset = f.roots.toFinset
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
NumberField.mixedEmbedding.normAtComplexPlaces_polarSpaceCoord_symm : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] (x : NumberField.mixedEmbedding.polarSpace K),
  NumberField.mixedEmbedding.normAtComplexPlaces (↑(NumberField.mixedEmbedding.polarSpaceCoord K).symm x) =
    NumberField.mixedEmbedding.normAtComplexPlaces (NumberField.mixedEmbedding.mixedSpaceOfRealSpace x.1)
-- Mathlib.Topology.MetricSpace.Snowflaking
Metric.Snowflaking.preimage_toSnowflaking_closedBall : ∀ {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} [inst : PseudoMetricSpace X] (x : Metric.Snowflaking X α hα₀ hα₁)
  {r : ℝ},
  0 ≤ r →
    ⇑Metric.Snowflaking.toSnowflaking ⁻¹' Metric.closedBall x r =
      Metric.closedBall (Metric.Snowflaking.ofSnowflaking x) (r ^ α⁻¹)
-- Lean.Elab.PreDefinition.FixedParams
/-- If `value` is the body of the `funIdx`'s function, instantiate the fixed parameters.
Expects enough manifest lambdas to instantiate all fixed parameters, but can handle
eta-contracted definitions beyond that.
 -/
Lean.Elab.FixedParamPerm.instantiateLambda : Lean.Elab.FixedParamPerm → Lean.Expr → Array Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Analysis.SpecialFunctions.Sqrt
Differentiable.sqrt : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ},
  Differentiable ℝ f → (∀ (x : E), f x ≠ 0) → Differentiable ℝ fun y => √(f y)
-- Mathlib.Algebra.FreeMonoid.Basic
/-- Equivalence between maps `α → M` and monoid homomorphisms `FreeMonoid α →* M`.  -/
FreeMonoid.lift : {α : Type u_1} → {M : Type u_4} → [inst : Monoid M] → (α → M) ≃ (FreeMonoid α →* M)
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.HasCoseparator.hasCodetector : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Balanced C]
  [CategoryTheory.HasCoseparator C], CategoryTheory.HasCodetector C
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.size_right_le_size_union : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashSet.Raw α} [EquivBEq α] [LawfulHashable α],
  m₁.WF → m₂.WF → m₂.size ≤ (m₁ ∪ m₂).size
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.infinitePos_iff : ∀ {x : ℝ*}, x.InfinitePos ↔ 0 < x ∧ ArchimedeanClass.mk x < 0
-- Mathlib.Data.Set.Image
Set.image_inter_preimage : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (s : Set α) (t : Set β), f '' (s ∩ f ⁻¹' t) = f '' s ∩ t
-- Lean.Elab.Do.Basic
/-- Prepare the context for elaborating the body of a `do` block that does not support `mut` vars,
`break`, `continue` or `return`.
 -/
Lean.Elab.Do.withoutControl : Lean.Elab.Do.DoElabM Lean.Expr → Lean.Elab.Do.DoElabM Lean.Expr
-- Mathlib.Data.Matrix.Basic
AddEquiv.mapMatrix_symm : ∀ {m : Type u_2} {n : Type u_3} {α : Type u_11} {β : Type u_12} [inst : Add α] [inst_1 : Add β] (f : α ≃+ β),
  f.mapMatrix.symm = f.symm.mapMatrix
-- Init.Data.Option.Lemmas
Option.join_ne_none' : ∀ {α : Type u_1} {x : Option (Option α)}, ¬x.join = none ↔ ∃ z, x = some (some z)
-- Mathlib.Geometry.Manifold.ContMDiff.Defs
/-- **Alias** of the forward direction of `contMDiffWithinAt_insert_self`. -/
ContMDiffWithinAt.of_insert : ∀ {𝕜 : 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] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {s : Set M} {x : M}
  {n : WithTop ℕ∞}, ContMDiffWithinAt I I' n f (insert x s) x → ContMDiffWithinAt I I' n f s x
-- Mathlib.Algebra.Homology.Embedding.Boundary
ComplexShape.boundaryLE_embeddingUpIntLE_iff : ∀ (p : ℤ) (n : ℕ), (ComplexShape.embeddingUpIntLE p).BoundaryLE n ↔ n = 0
-- Init.Data.Nat.Fold
Nat.any_zero : ∀ {f : (i : ℕ) → i < 0 → Bool}, Nat.any 0 f = false
-- Mathlib.Topology.Connected.PathConnected
PathConnectedSpace.connectedSpace : ∀ {X : Type u_1} [inst : TopologicalSpace X] [PathConnectedSpace X], ConnectedSpace X
-- Init.Data.String.PosRaw
String.Pos.Raw.mk_zero : { } = 0
-- Mathlib.ModelTheory.Definability
/-- `TermDefinable₁` is defined as `TermDefinable` on the `Unit` index type.  -/
Set.termDefinable₁_iff_termDefinable : ∀ {M : Type w} {A : Set M} {L : FirstOrder.Language} [inst : L.Structure M] (f : M → M),
  Set.TermDefinable₁ L f ↔ A.TermDefinable L fun v => f (v ())
-- Mathlib.RingTheory.PowerSeries.Basic
Polynomial.coe_smul : ∀ {R : Type u_1} [inst : Semiring R] (φ : Polynomial R) (r : R), ↑(r • φ) = r • ↑φ
-- Mathlib.CategoryTheory.GradedObject.Unitor
CategoryTheory.GradedObject.TriangleIndexData.r_zero : ∀ {I₁ : Type u_1} {I₂ : Type u_2} {I₃ : Type u_3} {J : Type u_4} [inst : Zero I₂] {r : I₁ × I₂ × I₃ → J}
  {π : I₁ × I₃ → J} (τ : CategoryTheory.GradedObject.TriangleIndexData r π) (i₁ : I₁) (i₃ : I₃),
  r (i₁, 0, i₃) = π (i₁, i₃)
-- Mathlib.Data.List.Map2
List.map₂Right_eq_zipWith : ∀ {α : Type u} {β : Type v} {γ : Type w} (f : Option α → β → γ) (as : List α) (bs : List β),
  bs.length ≤ as.length → List.map₂Right f as bs = List.zipWith (fun a b => f (some a) b) as bs
-- Mathlib.Algebra.Group.Subgroup.Lattice
/-- The inf of two `AddSubgroup`s is their intersection.  -/
AddSubgroup.instMin : {G : Type u_1} → [inst : AddGroup G] → Min (AddSubgroup G)
-- Mathlib.Analysis.Calculus.DerivativeTest
/-- If `f` is continuous at `b` and differentiable on `Ioo a b`, then `f` is continuous on
`Ioc a b`.  -/
_private.Mathlib.Analysis.Calculus.DerivativeTest.0.continuousOn_Ioc : ∀ {f : ℝ → ℝ} {a b : ℝ}, ContinuousAt f b → DifferentiableOn ℝ f (Set.Ioo a b) → ContinuousOn f (Set.Ioc a b)
-- Mathlib.Topology.Bases
TopologicalSpace.isSeparable_pi : ∀ {ι : Type u_2} [Countable ι] {α : ι → Type u_3} {s : (i : ι) → Set (α i)} [inst : (i : ι) → TopologicalSpace (α i)],
  (∀ (i : ι), TopologicalSpace.IsSeparable (s i)) → TopologicalSpace.IsSeparable {f | ∀ (i : ι), f i ∈ s i}
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.minKey?_insertIfNew_of_isEmpty : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β k}, t.isEmpty = true → (t.insertIfNew k v).minKey? = some k
-- Mathlib.CategoryTheory.CodiscreteCategory
/-- Right triangle equality of the adjunction `Cat.objects ⊣ Codiscrete.functorToCat`,
stated using a composition of functors.  -/
CategoryTheory.Codiscrete.right_triangle_components : ∀ (X : Type u),
  (CategoryTheory.Codiscrete.unitApp (CategoryTheory.Codiscrete X)).comp
      (CategoryTheory.Codiscrete.functorOfFun (CategoryTheory.Codiscrete.counitApp X)) =
    CategoryTheory.Functor.id (CategoryTheory.Codiscrete X)
-- Mathlib.Analysis.InnerProductSpace.Adjoint
LinearMap.isStarProjection_iff_isSymmetricProjection : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : FiniteDimensional 𝕜 E] {T : E →ₗ[𝕜] E}, IsStarProjection T ↔ T.IsSymmetricProjection
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenSubgroup.mem_toOpens : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] {U : OpenSubgroup G} {g : G}, g ∈ ↑U ↔ g ∈ U
-- Mathlib.Dynamics.PeriodicPts.Defs
Function.nodup_periodicOrbit : ∀ {α : Type u_1} {f : α → α} {x : α}, (Function.periodicOrbit f x).Nodup
-- Std.Data.TreeSet.Basic
/-- Two tree sets are equivalent in the sense of Equiv iff all the values are equal.  -/
Std.TreeSet.«term_~m_» : Lean.TrailingParserDescr
-- Lean.PrettyPrinter.Delaborator.Builtins
Lean.PrettyPrinter.Delaborator.AppMatchState.mk.injEq : ∀ (info : Lean.Meta.MatcherInfo) (matcherTy : Lean.SubExpr) (motive : Option (Lean.Term × Lean.Expr))
  (motiveNamed : Bool) (discrs : Array Lean.Term) (hNames? : Array (Option Lean.Name)) (alts : Array Lean.SubExpr)
  (varNames : Array (Array Lean.Name)) (rhss : Array Lean.Term) (info_1 : Lean.Meta.MatcherInfo)
  (matcherTy_1 : Lean.SubExpr) (motive_1 : Option (Lean.Term × Lean.Expr)) (motiveNamed_1 : Bool)
  (discrs_1 : Array Lean.Term) (hNames?_1 : Array (Option Lean.Name)) (alts_1 : Array Lean.SubExpr)
  (varNames_1 : Array (Array Lean.Name)) (rhss_1 : Array Lean.Term),
  ({ info := info, matcherTy := matcherTy, motive := motive, motiveNamed := motiveNamed, discrs := discrs,
        hNames? := hNames?, alts := alts, varNames := varNames, rhss := rhss } =
      { info := info_1, matcherTy := matcherTy_1, motive := motive_1, motiveNamed := motiveNamed_1, discrs := discrs_1,
        hNames? := hNames?_1, alts := alts_1, varNames := varNames_1, rhss := rhss_1 }) =
    (info = info_1 ∧
      matcherTy = matcherTy_1 ∧
        motive = motive_1 ∧
          motiveNamed = motiveNamed_1 ∧
            discrs = discrs_1 ∧ hNames? = hNames?_1 ∧ alts = alts_1 ∧ varNames = varNames_1 ∧ rhss = rhss_1)
-- Mathlib.Order.Monotone.Basic
StrictAnti.lt_iff_gt : ∀ {α : Type u} {β : Type v} [inst : LinearOrder α] [inst_1 : Preorder β] {f : α → β},
  StrictAnti f → ∀ {a b : α}, f a < f b ↔ b < a
-- Lean.Environment
_private.Lean.Environment.0.Lean.readModuleDataParts.unsafe_1 : System.FilePath → Array Lean.CompactedRegion → IO (Lean.ModuleData × Lean.CompactedRegion)
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.RelCWComplex.base_subset_complex : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [Topology.RelCWComplex C D], D ⊆ C
-- Mathlib.Order.WellFoundedSet
/-- A subset of a preorder is partially well-ordered when any infinite sequence contains
a monotone subsequence of length 2 (or equivalently, an infinite monotone subsequence).  -/
Set.IsPWO : {α : Type u_2} → [Preorder α] → Set α → Prop
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Matrix.GeneralLinearGroup.val_det_apply : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] (A : GL n R),
  ↑(Matrix.GeneralLinearGroup.det A) = (↑A).det
-- Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
ZMod.ringEquivCongr.congr_simp : ∀ {m n : ℕ} (h : m = n), ZMod.ringEquivCongr h = ZMod.ringEquivCongr h
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
CategoryTheory.Limits.reflectsColimitsOfShape_subsingleton : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (J : Type w) [inst_2 : CategoryTheory.Category.{w', w} J] (F : CategoryTheory.Functor C D),
  Subsingleton (CategoryTheory.Limits.ReflectsColimitsOfShape J F)
-- Mathlib.Order.Defs.Unbundled
RelLowerSet.mk.injEq : ∀ {α : Type u_1} [inst : LE α] {P : α → Prop} (carrier : Set α) (isRelLowerSet' : IsRelLowerSet carrier P)
  (carrier_1 : Set α) (isRelLowerSet'_1 : IsRelLowerSet carrier_1 P),
  ({ carrier := carrier, isRelLowerSet' := isRelLowerSet' } =
      { carrier := carrier_1, isRelLowerSet' := isRelLowerSet'_1 }) =
    (carrier = carrier_1)
-- Mathlib.MeasureTheory.Measure.Haar.Basic
MeasureTheory.Measure.addHaarMeasure_self : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalAddGroup G]
  [inst_3 : MeasurableSpace G] [inst_4 : BorelSpace G] {K₀ : TopologicalSpace.PositiveCompacts G},
  (MeasureTheory.Measure.addHaarMeasure K₀) ↑K₀ = 1
-- Mathlib.Geometry.Manifold.Algebra.LieGroup
ContMDiffWithinAt.div₀ : ∀ {𝕜 : 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 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : GroupWithZero G] [ContMDiffInv₀ I n G]
  [ContMDiffMul I n G] {E' : Type u_5} [inst_9 : NormedAddCommGroup E'] [inst_10 : NormedSpace 𝕜 E'] {H' : Type u_6}
  [inst_11 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [inst_12 : TopologicalSpace M]
  [inst_13 : ChartedSpace H' M] {f g : M → G} {s : Set M} {a : M},
  ContMDiffWithinAt I' I n f s a → ContMDiffWithinAt I' I n g s a → g a ≠ 0 → ContMDiffWithinAt I' I n (f / g) s a
-- Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
/-- A category with finite biproducts and finite limits is AB4 if it is AB5.  -/
CategoryTheory.AB4.of_AB5 : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasFiniteLimits C]
  [inst_4 : CategoryTheory.Limits.HasFilteredColimitsOfSize.{w, w, v, u} C] [CategoryTheory.AB5OfSize.{w, w, v, u} C],
  CategoryTheory.AB4OfSize.{w, v, u} C
-- Mathlib.CategoryTheory.Monad.Algebra
CategoryTheory.Comonad.cofree_obj_a : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (G : CategoryTheory.Comonad C) (X : C),
  (G.cofree.obj X).a = G.δ.app X
-- Lean.Meta.Tactic.Grind.EMatchTheoremParam
_private.Lean.Meta.Tactic.Grind.EMatchTheoremParam.0.Lean.Meta.Grind.toInstantiateParam : Lean.TSyntax [`Lean.Parser.Tactic.grindLemma, `Lean.Parser.Tactic.grindLemmaMin] →
  Lean.TSyntax `Lean.Parser.Tactic.Grind.thm
-- Init.Data.SInt.Lemmas
Int64.sub_zero : ∀ (a : Int64), a - 0 = a
-- Init.Internal.Order.Lemmas
Lean.Order.Array.monotone_array_forM : ∀ {m : Type u → Type v} [inst : Monad m] [inst_1 : (α : Type u) → Lean.Order.PartialOrder (m α)] [Lean.Order.MonoBind m]
  {α : Type u} {γ : Type w} [inst_3 : Lean.Order.PartialOrder γ] (f : γ → α → m PUnit.{u + 1}) (xs : Array α)
  (start stop : ℕ), Lean.Order.monotone f → Lean.Order.monotone fun x => Array.forM (f x) xs start stop
-- Mathlib.NumberTheory.LocalField.Basic
IsNonarchimedeanLocalField.instIsTopologicalDivisionRing : ∀ (K : Type u_1) [inst : Field K] [inst_1 : ValuativeRel K] [inst_2 : TopologicalSpace K]
  [IsNonarchimedeanLocalField K], IsTopologicalDivisionRing K
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKeyD_insert_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {a fallback : α} {b : β a}, (t.insert a b).getKeyD a fallback = a
-- Mathlib.Order.Partition.Basic
/-- Every partition has a representative function.  -/
Partition.IsRepFun.nonempty : ∀ {α : Type u_1} {u : Set α} (P : Partition u), ∃ f, P.IsRepFun f
-- ProofWidgets.Data.Html
ProofWidgets.Jsx.«proofWidgetsJsxElement<__/>» : Lean.ParserDescr
-- Mathlib.Algebra.Category.MonCat.Basic
MonCat.hom_ext : ∀ {M N : MonCat} {f g : M ⟶ N}, MonCat.Hom.hom f = MonCat.Hom.hom g → f = g
-- Mathlib.LinearAlgebra.Matrix.Module
/-- `Mⁿ` is a `Mₙ(R)` module, note that this creates a diamond when `M` is `Matrix ι ι R` or when
`M` is `R`.  -/
Matrix.Module.matrixModule : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_3} →
      [inst : Ring R] →
        [inst_1 : Fintype ι] →
          [inst_2 : DecidableEq ι] → [inst_3 : AddCommGroup M] → [Module R M] → Module (Matrix ι ι R) (ι → M)
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.SimplicialObject.Augmented.const_obj_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : C),
  (CategoryTheory.SimplicialObject.Augmented.const.obj X).hom =
    CategoryTheory.CategoryStruct.id
      ((CategoryTheory.Functor.id (CategoryTheory.SimplicialObject C)).obj
        ((CategoryTheory.SimplicialObject.const C).obj X))