mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.Embedding.IsSupported
HomologicalComplex.isStrictlySupportedOutside_op_iff : ∀ {ι : 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'),
  K.op.IsStrictlySupportedOutside e.op ↔ K.IsStrictlySupportedOutside e
-- Mathlib.Data.Fin.Basic
Fin.default_eq_zero : ∀ (n : ℕ) [inst : NeZero n], default = 0
-- Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory
/-- If `A` and `B` are triangulated subcategories of a (pre)triangulated
category `C` (with `B` closed under isomorphisms), we say that `A` is
left `B`-localizing if any morphism `X ⟶ Y` with `X` in `A` and
`Y` in `B` factors through an object that is in `A` and `B`.
Note that the definition does not use the (pre)triangulated structure:
see `isVerdierLeftLocalizing_iff` for a characterization which
relies on it.  -/
CategoryTheory.ObjectProperty.IsVerdierLeftLocalizing : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    CategoryTheory.ObjectProperty C → CategoryTheory.ObjectProperty C → Prop
-- Mathlib.GroupTheory.GroupAction.Quotient
AddAction.selfEquivOrbitsQuotientProd.eq_1 : ∀ {G : Type u} {X : Type v} [inst : AddGroup G] [inst_1 : AddAction G X] (h : ∀ (b : X), AddAction.stabilizer G b = ⊥),
  AddAction.selfEquivOrbitsQuotientProd h = AddAction.selfEquivOrbitsQuotientProd' ⋯ h
-- Batteries.Recycling.RBTree.Alter
RBTree.RBNode.Path.ins.eq_def : ∀ {α : Type u_1} (x : RBTree.RBNode.Path α) (x_1 : RBTree.RBNode α),
  x.ins x_1 =
    match x, x_1 with
    | RBTree.RBNode.Path.root, t => t.setBlack
    | RBTree.RBNode.Path.left RBTree.RBColor.red parent y b, a =>
      parent.ins (RBTree.RBNode.node RBTree.RBColor.red a y b)
    | RBTree.RBNode.Path.right RBTree.RBColor.red a y parent, b =>
      parent.ins (RBTree.RBNode.node RBTree.RBColor.red a y b)
    | RBTree.RBNode.Path.left RBTree.RBColor.black parent y b, a => parent.ins (a.balance1 y b)
    | RBTree.RBNode.Path.right RBTree.RBColor.black a y parent, b => parent.ins (a.balance2 y b)
-- Mathlib.Algebra.Opposites
MulOpposite.instInv : {α : Type u_1} → [Inv α] → Inv αᵐᵒᵖ
-- Mathlib.AlgebraicTopology.SimplicialNerve
CategoryTheory.SimplicialThickening.Path.right : ∀ {J : Type u_1} [inst : LinearOrder J] {i j : J} (self : CategoryTheory.SimplicialThickening.Path i j), j ∈ self.I
-- Mathlib.Topology.Inseparable
Specializes.mem_closed : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X} {s : Set X}, x ⤳ y → IsClosed s → x ∈ s → y ∈ s
-- Lean.Elab.ConfigEval.Commands
/-- `ensure_eval_expr_instance t` ensures there is a `ConfigItem.EvalExpr t` instance by
deriving one or more instances if it needs to.
 -/
Lean.Elab.ConfigEval.ensureEvalExprInstance : Lean.ParserDescr
-- Mathlib.Data.Set.Card
Set.one_lt_encard_iff : ∀ {α : Type u_1} {s : Set α}, 1 < s.encard ↔ ∃ a b, a ∈ s ∧ b ∈ s ∧ a ≠ b
-- Mathlib.Data.Nat.Notation
/-- The natural numbers, starting at zero.

This type is special-cased by both the kernel and the compiler, and overridden with an efficient
implementation. Both use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.
 -/
termℕ : Lean.ParserDescr
-- Mathlib.Order.RelIso.Basic
RelIso.compl_apply : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ≃r s) (a : α), f.compl a = f a
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral
/-- An integrability criterion for the continuous functional calculus.
For a version with stronger assumptions which in practice are often easier to verify, see
`integrableOn_cfcₙ`.  -/
integrableOn_cfcₙ' : ∀ {X : Type u_1} {𝕜 : Type u_2} {A : Type u_3} {p : A → Prop} [inst : RCLike 𝕜] [inst_1 : MeasurableSpace X]
  {μ : MeasureTheory.Measure X} [inst_2 : NonUnitalNormedRing A] [inst_3 : StarRing A] [inst_4 : NormedSpace 𝕜 A]
  [inst_5 : IsScalarTower 𝕜 A A] [inst_6 : SMulCommClass 𝕜 A A] [inst_7 : NonUnitalContinuousFunctionalCalculus 𝕜 A p]
  [inst_8 : CompleteSpace A] {s : Set X} (f : X → 𝕜 → 𝕜) (a : A),
  MeasureTheory.IntegrableOn (fun x => ContinuousMapZero.mkD ((quasispectrum 𝕜 a).domRestrict (f x)) 0) s μ →
    autoParam (p a) integrableOn_cfcₙ'._auto_1 → MeasureTheory.IntegrableOn (fun x => cfcₙ (f x) a) s μ
-- Init.Data.String.Pattern.Basic
InvImage.eq_1 : ∀ {α : Sort u} {β : Sort v} (r : β → β → Prop) (f : α → β) (a₁ a₂ : α), InvImage r f a₁ a₂ = r (f a₁) (f a₂)
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
CFC.nnrpow_eq_nnrpow_pi : ∀ {ι : Type u_2} {C : ι → Type u_3} [inst : (i : ι) → PartialOrder (C i)] [inst_1 : (i : ι) → NonUnitalRing (C i)]
  [inst_2 : (i : ι) → TopologicalSpace (C i)] [inst_3 : (i : ι) → StarRing (C i)]
  [inst_4 : ∀ (i : ι), StarOrderedRing (C i)] [inst_5 : StarOrderedRing ((i : ι) → C i)]
  [inst_6 : (i : ι) → Module ℝ (C i)] [inst_7 : ∀ (i : ι), SMulCommClass ℝ (C i) (C i)]
  [inst_8 : ∀ (i : ι), IsScalarTower ℝ (C i) (C i)]
  [inst_9 : ∀ (i : ι), NonUnitalContinuousFunctionalCalculus ℝ (C i) IsSelfAdjoint]
  [inst_10 : NonUnitalContinuousFunctionalCalculus ℝ ((i : ι) → C i) IsSelfAdjoint]
  [∀ (i : ι), IsSemitopologicalRing (C i)] [∀ (i : ι), T2Space (C i)] [inst_13 : NonnegSpectrumClass ℝ ((i : ι) → C i)]
  [inst_14 : ∀ (i : ι), NonnegSpectrumClass ℝ (C i)] {c : (i : ι) → C i} {x : NNReal},
  autoParam (∀ (i : ι), 0 ≤ c i) CFC.nnrpow_eq_nnrpow_pi._auto_1 → CFC.nnrpow c x = c ^ x
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
/-- An even function is interval integrable (with respect to the volume measure) on every interval
if it is interval integrable (with respect to the volume measure) on every interval of the form
`0..x`, for positive `x`.  -/
intervalIntegrable_of_even : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] {f : ℝ → E},
  (∀ (x : ℝ), f x = f (-x)) →
    (∀ (x : ℝ), 0 < x → IntervalIntegrable f MeasureTheory.volume 0 x) →
      ∀ {a b : ℝ},
        autoParam (‖f (min 0 a)‖ₑ ≠ ⊤) intervalIntegrable_of_even._auto_1 →
          autoParam (‖f (min 0 b)‖ₑ ≠ ⊤) intervalIntegrable_of_even._auto_3 →
            IntervalIntegrable f MeasureTheory.volume a b
-- Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
/-- The unique existence of an inverse to `spine X n` forall `n : ℕ` implies
the mere existence of such an inverse.  -/
SSet.StrictSegal.isStrictSegal : ∀ {X : SSet} (sx : X.StrictSegal), X.IsStrictSegal
-- Init.Data.Array.Lemmas
Array.map_const_fun : ∀ {β : Type u_1} {α : Type u_2} {x : β}, Array.map (Function.const α x) = fun x_1 => Array.replicate x_1.size x
-- Mathlib.Topology.MetricSpace.IsometricSMul
/-- **Alias** of `Metric.smul_eball`. -/
EMetric.smul_ball : ∀ {G : Type v} {X : Type w} [inst : PseudoEMetricSpace X] [inst_1 : Group G] [inst_2 : MulAction G X]
  [IsIsometricSMul G X] (c : G) (x : X) (r : ENNReal), c • Metric.eball x r = Metric.eball (c • x) r
-- Init.Data.Range.Basic
Std.Legacy.Range.step : Std.Legacy.Range → ℕ
-- Mathlib.Data.Nat.Sqrt
Nat.sqrt_pos : ∀ {n : ℕ}, 0 < n.sqrt ↔ 0 < n
-- Mathlib.Topology.ContinuousMap.ContinuousMapZero
/-- **Alias** of `ContinuousMapZero.continuous_precomp`. -/
ContinuousMapZero.continuous_comp_left : ∀ {X : Type u_1} {Y : Type u_2} {R : Type u_3} [inst : Zero X] [inst_1 : Zero Y] [inst_2 : Zero R]
  [inst_3 : TopologicalSpace X] [inst_4 : TopologicalSpace Y] [inst_5 : TopologicalSpace R] (f : ContinuousMapZero X Y),
  Continuous fun g => g.comp f
-- Mathlib.Data.Multiset.DershowitzManna
/-- The standard Dershowitz–Manna ordering.  -/
Multiset.IsDershowitzMannaLT : {α : Type u_1} → [Preorder α] → Multiset α → Multiset α → Prop
-- Init.Data.BitVec.Lemmas
BitVec.getElem_eq_extractLsb' : ∀ {w : ℕ} (x : BitVec w) (i : ℕ) (h : i < w), x[i] = (BitVec.extractLsb' i 1 x == 1#1)
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.coe_one : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : One β], ⇑1 = 1
-- Std.Time.DateTime
Std.Time.DateTime.instHAddDuration : HAdd Std.Time.DateTime Std.Time.Duration Std.Time.DateTime
-- Mathlib.Analysis.CStarAlgebra.Basic
symm_starₗᵢ : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : CommSemiring 𝕜] [inst_1 : StarRing 𝕜] [inst_2 : SeminormedAddCommGroup E]
  [inst_3 : StarAddMonoid E] [inst_4 : NormedStarGroup E] [inst_5 : Module 𝕜 E] [inst_6 : StarModule 𝕜 E],
  (starₗᵢ 𝕜).symm = starₗᵢ 𝕜
-- Mathlib.Tactic.Sat.FromLRAT
/-- A proof of `⊢ ctx.proof c`.
Note that we do not use `have` statements to cache these proofs:
this is literally the proof expression itself. As a result, the proof terms
rely heavily on dag-like sharing of the expression, and printing these proof terms
directly is likely to crash lean for larger examples.  -/
Mathlib.Tactic.Sat.Clause.proof : Mathlib.Tactic.Sat.Clause → Lean.Expr
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.leftUnitor_neg_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X : CategoryTheory.AddMon C),
  (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv.hom =
    (CategoryTheory.MonoidalCategoryStruct.leftUnitor X.X).inv
-- Mathlib.Data.DFinsupp.Defs
/-- Like `Finsupp.single_eq_single_iff`, but with a `HEq` due to dependent types  -/
DFinsupp.single_eq_single_iff : ∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → Zero (β i)] [inst_1 : DecidableEq ι] (i j : ι) (xi : β i) (xj : β j),
  ((fun₀ | i => xi) = fun₀ | j => xj) ↔ i = j ∧ xi ≍ xj ∨ xi = 0 ∧ xj = 0
-- Mathlib.Algebra.Order.Field.Basic
inv_lt_inv_of_neg : ∀ {α : Type u_2} [inst : Field α] [inst_1 : PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] {a b : α},
  a < 0 → b < 0 → (a⁻¹ < b⁻¹ ↔ b < a)
-- Mathlib.Topology.Sets.Compacts
/-- The type of compact open sets of a topological space. This is useful in non-Hausdorff contexts,
in particular spectral spaces.  -/
TopologicalSpace.CompactOpens : (α : Type u_4) → [TopologicalSpace α] → Type u_4
-- Lean.Parser.Extension
Lean.Parser.AliasValue.const : {α : Type} → α → Lean.Parser.AliasValue α
-- Mathlib.Logic.Equiv.Set
Equiv.image_strictMono : ∀ {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] {e : α ≃ β} (s : Set α),
  StrictMono ⇑e → StrictMono ⇑(e.image s)
-- Mathlib.Algebra.Group.Hom.Defs
OneHom.copy.eq_1 : ∀ {M : Type u_4} {N : Type u_5} [inst : One M] [inst_1 : One N] (f : OneHom M N) (f' : M → N) (h : f' = ⇑f),
  f.copy f' h = { toFun := f', map_one' := ⋯ }
-- Mathlib.GroupTheory.SemidirectProduct
SemidirectProduct.map_right : ∀ {N₁ : Type u_4} {G₁ : Type u_5} {N₂ : Type u_6} {G₂ : Type u_7} [inst : Group N₁] [inst_1 : Group G₁]
  [inst_2 : Group N₂] [inst_3 : Group G₂] {φ₁ : G₁ →* MulAut N₁} {φ₂ : G₂ →* MulAut N₂} (fn : N₁ →* N₂) (fg : G₁ →* G₂)
  (h : ∀ (g : G₁), fn.comp (MulEquiv.toMonoidHom (φ₁ g)) = (MulEquiv.toMonoidHom (φ₂ (fg g))).comp fn)
  (g : N₁ ⋊[φ₁] G₁), ((SemidirectProduct.map fn fg h) g).right = fg g.right
-- Mathlib.Analysis.Calculus.Deriv.Basic
HasDerivAt.unique : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f₀' f₁' : F} {x : 𝕜}, HasDerivAt f f₀' x → HasDerivAt f f₁' x → f₀' = f₁'
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.continuous_ofLp : ∀ (p : ENNReal) {ι : Type u_2} (β : ι → Type u_4) [inst : (i : ι) → TopologicalSpace (β i)], Continuous WithLp.ofLp
-- Lean.Data.PersistentArray
Lean.PersistentArrayNode.leaf.injEq : ∀ {α : Type u} (vs vs_1 : Array α),
  (Lean.PersistentArrayNode.leaf vs = Lean.PersistentArrayNode.leaf vs_1) = (vs = vs_1)
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.Mor₂Iso.whiskerLeft : Lean.Expr →
  Mathlib.Tactic.BicategoryLike.Mor₁ →
    Mathlib.Tactic.BicategoryLike.Mor₁ →
      Mathlib.Tactic.BicategoryLike.Mor₁ → Mathlib.Tactic.BicategoryLike.Mor₂Iso → Mathlib.Tactic.BicategoryLike.Mor₂Iso
-- Lean.DocString.Formatter
_private.Lean.DocString.Formatter.0.Lean.Doc.Parser.versoSyntaxToString'.out : String → ReaderT ℕ (StateM String) Unit
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.Measure.IsAddHaarMeasure.smul : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : AddGroup G] [inst_2 : TopologicalSpace G]
  (μ : MeasureTheory.Measure G) [μ.IsAddHaarMeasure] {c : ENNReal}, c ≠ 0 → c ≠ ⊤ → (c • μ).IsAddHaarMeasure
-- Mathlib.Data.Finsupp.Defs
Finsupp.ext_iff : ∀ {α : Type u_1} {M : Type u_4} [inst : Zero M] {f g : α →₀ M}, f = g ↔ ∀ (a : α), f a = g a
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.instNeg : {E : Type u_2} →
  {F : Type u_3} →
    [inst : NormedAddCommGroup E] →
      [inst_1 : NormedSpace ℝ E] →
        [inst_2 : NormedAddCommGroup F] →
          [inst_3 : NormedSpace ℝ F] →
            {n : ℕ∞} → {K : TopologicalSpace.Compacts E} → Neg (ContDiffMapSupportedIn E F n K)
-- Mathlib.Tactic.TacticAnalysis.Declarations
_private.Mathlib.Tactic.TacticAnalysis.Declarations.0.Mathlib.TacticAnalysis.TerminalReplacementOutcome.remainingGoals.inj : ∀ {stx : Lean.TSyntax `tactic} {goals : List Lean.MessageData} {stx_1 : Lean.TSyntax `tactic}
  {goals_1 : List Lean.MessageData},
  Mathlib.TacticAnalysis.TerminalReplacementOutcome.remainingGoals✝ stx goals =
      Mathlib.TacticAnalysis.TerminalReplacementOutcome.remainingGoals✝ stx_1 goals_1 →
    stx = stx_1 ∧ goals = goals_1
-- Mathlib.Data.NNRat.Defs
Rat.toNNRat_pos : ∀ {q : ℚ}, 0 < q.toNNRat ↔ 0 < q
-- Mathlib.RingTheory.RamificationInertia.Ramification
Ideal.ramificationIdx_below_dvd : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  [inst_3 : Algebra R S] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [IsScalarTower R S T] (q : Ideal S) (r : Ideal T)
  [r.LiesOver q] [Module.Flat S T], q.ramificationIdx R ∣ r.ramificationIdx R
-- Mathlib.RingTheory.Regular.RegularSequence
RingTheory.Sequence.isWeaklyRegular_cons_iff' : ∀ {R : Type u_1} (M : Type u_3) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (r : R)
  (rs : List R),
  RingTheory.Sequence.IsWeaklyRegular M (r :: rs) ↔
    IsSMulRegular M r ∧
      RingTheory.Sequence.IsWeaklyRegular (QuotSMulTop r M) (List.map (⇑(Ideal.Quotient.mk (Ideal.span {r}))) rs)
-- Mathlib.Order.GaloisConnection.Defs
/-- The Galois connection associated to a Galois insertion.  -/
GaloisInsertion.gc : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {l : α → β} {u : β → α}
  (self : GaloisInsertion l u), GaloisConnection l u
-- Mathlib.LinearAlgebra.DirectSum.Finsupp
TensorProduct.finsuppLeft_apply_tmul : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] {M : Type u_3}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Module S M] [inst_6 : IsScalarTower R S M] {N : Type u_4}
  [inst_7 : AddCommMonoid N] [inst_8 : Module R N] {ι : Type u_5} [inst_9 : DecidableEq ι] (p : ι →₀ M) (n : N),
  (TensorProduct.finsuppLeft R S M N ι) (p ⊗ₜ[R] n) = p.sum fun i m => fun₀ | i => m ⊗ₜ[R] n
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.coe_domRestrict : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β]
  (f : BoundedContinuousFunction α β) (s : Set α), ⇑(f.domRestrict s) = ⇑f ∘ Subtype.val
-- Mathlib.Topology.Specialization
Specialization.isUpperSet_ofEquiv_preimage : ∀ {α : Type u_1} [inst : TopologicalSpace α] [AlexandrovDiscrete α] {s : Set α},
  IsUpperSet (⇑Specialization.ofEquiv ⁻¹' s) ↔ IsOpen s
-- Mathlib.GroupTheory.Transfer
MonoidHom.transfer_def : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} {A : Type u_2} [inst_1 : CommGroup A] (ϕ : ↥H →* A)
  (T : H.LeftTransversal) [inst_2 : H.FiniteIndex] (g : G), ϕ.transfer g = Subgroup.leftTransversals.diff ϕ T (g • T)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.size_le_size_insertIfNew : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β k}, t.size ≤ (t.insertIfNew k v).size
-- Mathlib.GroupTheory.Abelianization.Defs
Abelianization.map_comp : ∀ {G : Type u} [inst : Group G] {H : Type v} [inst_1 : Group H] (f : G →* H) {I : Type w} [inst_2 : Group I]
  (g : H →* I), (Abelianization.map g).comp (Abelianization.map f) = Abelianization.map (g.comp f)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.getKey!_ofList_of_contains_eq_false : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} [EquivBEq α] [LawfulHashable α] [inst : Inhabited α]
  {l : List (α × β)} {k : α},
  (List.map Prod.fst l).contains k = false → (Std.DHashMap.Const.ofList l).getKey! k = default
-- Mathlib.Data.List.Destutter
List.destutter'_ne_nil : ∀ {α : Type u_1} (l : List α) (R : α → α → Prop) [inst : DecidableRel R] {a : α}, List.destutter' R a l ≠ []
-- Mathlib.Data.Finset.Empty
Finset.mk_zero : ∀ {α : Type u_1}, { val := 0, nodup := ⋯ } = ∅
-- Mathlib.MeasureTheory.Function.SimpleFuncDense
MeasureTheory.SimpleFunc.nearestPtInd.eq_def : ∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : PseudoEMetricSpace α] [inst_2 : OpensMeasurableSpace α]
  (e : ℕ → α) (x : ℕ),
  MeasureTheory.SimpleFunc.nearestPtInd e x =
    match x with
    | 0 => MeasureTheory.SimpleFunc.const α 0
    | N.succ =>
      MeasureTheory.SimpleFunc.piecewise (⋂ k, ⋂ (_ : k ≤ N), {x | edist (e (N + 1)) x < edist (e k) x}) ⋯
        (MeasureTheory.SimpleFunc.const α (N + 1)) (MeasureTheory.SimpleFunc.nearestPtInd e N)
-- Mathlib.Data.List.Defs
List.map₂Left'.eq_3 : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → Option β → γ) (a : α) (as : List α) (b : β) (bs : List β),
  List.map₂Left' f (a :: as) (b :: bs) = (f a (some b) :: (List.map₂Left' f as bs).1, (List.map₂Left' f as bs).2)
-- Mathlib.Analysis.Normed.Unbundled.AlgebraNorm
/-- An algebra norm on an `R`-algebra `S` is a ring norm on `S` compatible with the
action of `R`.  -/
AlgebraNorm : (R : Type u_1) → [inst : SeminormedCommRing R] → (S : Type u_2) → [inst_1 : Ring S] → [Algebra R S] → Type u_2
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.Precoverage.Small.zeroHypercoverSmall : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {J : CategoryTheory.Precoverage C} [self : J.Small] {S : C}
  (E : J.ZeroHypercover S), E.Small
-- Init.Data.BitVec.Lemmas
BitVec.and_allOnes : ∀ {w : ℕ} {x : BitVec w}, x &&& BitVec.allOnes w = x
-- Mathlib.CategoryTheory.Galois.Basic
CategoryTheory.PreGaloisCategory.FiberFunctor.mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] [inst_1 : CategoryTheory.PreGaloisCategory C]
  {F : CategoryTheory.Functor C FintypeCat},
  autoParam (CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) F)
      CategoryTheory.PreGaloisCategory.FiberFunctor.preservesTerminalObjects._autoParam →
    autoParam (CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingCospan F)
        CategoryTheory.PreGaloisCategory.FiberFunctor.preservesPullbacks._autoParam →
      autoParam (CategoryTheory.Limits.PreservesFiniteCoproducts F)
          CategoryTheory.PreGaloisCategory.FiberFunctor.preservesFiniteCoproducts._autoParam →
        autoParam F.PreservesEpimorphisms CategoryTheory.PreGaloisCategory.FiberFunctor.preservesEpis._autoParam →
          autoParam
              (∀ (G : Type u₂) [inst_2 : Group G] [Finite G],
                CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.SingleObj G) F)
              CategoryTheory.PreGaloisCategory.FiberFunctor.preservesQuotientsByFiniteGroups._autoParam →
            autoParam F.ReflectsIsomorphisms CategoryTheory.PreGaloisCategory.FiberFunctor.reflectsIsos._autoParam →
              CategoryTheory.PreGaloisCategory.FiberFunctor F
-- Mathlib.Analysis.Normed.Group.Defs
ENormedMonoid.toESeminormedMonoid : {E : Type u_8} → {inst : TopologicalSpace E} → [self : ENormedMonoid E] → ESeminormedMonoid E
-- Mathlib.Computability.TuringMachine.Computable
Turing.inhabitedTM2Computable : Inhabited (Turing.TM2Computable Computability.encodeBool Computability.encodeBool id)
-- Lean.DocString.Syntax
/-- Boolean flag, turned on  -/
Lean.Doc.Syntax.flag_on : Lean.ParserDescr
-- Mathlib.SetTheory.ZFC.PSet
PSet.equiv_empty : ∀ (x : PSet.{u_1}) [IsEmpty x.Type], x.Equiv ∅
-- Mathlib.Topology.Connected.PathConnected
Joined.trans : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y z : X}, Joined x y → Joined y z → Joined x z
-- Mathlib.Algebra.Algebra.Spectrum.Basic
/-- Conjugation by a unit preserves the spectrum, inverse on left.  -/
spectrum.units_conjugate' : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Ring A] [inst_2 : Algebra R A] {a : A} {u : Aˣ},
  spectrum R (↑u⁻¹ * a * ↑u) = spectrum R a
-- Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting
CategoryTheory.HasLiftingProperty.transfiniteComposition.wellOrderInductionData.liftHom.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : LinearOrder J] [inst_2 : OrderBot J]
  {F : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.Cocone F} {X Y : C} {p : X ⟶ Y} {f : F.obj ⊥ ⟶ X}
  {g : c.pt ⟶ Y} [inst_3 : F.IsWellOrderContinuous] {j : J} (hj : Order.IsSuccLimit j)
  (s s_1 : ↑(⋯.functor.op.comp (CategoryTheory.HasLiftingProperty.transfiniteComposition.sqFunctor c p f g)).sections),
  s = s_1 →
    CategoryTheory.HasLiftingProperty.transfiniteComposition.wellOrderInductionData.liftHom hj s =
      CategoryTheory.HasLiftingProperty.transfiniteComposition.wellOrderInductionData.liftHom hj s_1
-- Mathlib.Analysis.Normed.Group.Basic
SeminormedCommGroup.induced.eq_1 : ∀ {𝓕 : Type u_1} (E : Type u_5) (F : Type u_6) [inst : FunLike 𝓕 E F] [inst_1 : CommGroup E]
  [inst_2 : SeminormedGroup F] [inst_3 : MonoidHomClass 𝓕 E F] (f : 𝓕),
  SeminormedCommGroup.induced E F f =
    { norm := fun a => ‖f a‖, toCommGroup := inst_1, dist := fun a a_1 => dist (f a) (f a_1), dist_self := ⋯,
      dist_comm := ⋯, dist_triangle := ⋯, edist := fun a a_1 => PseudoMetricSpace.edist (f a) (f a_1), edist_dist := ⋯,
      toUniformSpace :=
        { toTopologicalSpace := TopologicalSpace.induced (⇑f) PseudoMetricSpace.toUniformSpace.toTopologicalSpace,
          uniformity := Filter.comap (fun p => (f p.1, f p.2)) (uniformity F), symm := ⋯, comp := ⋯,
          nhds_eq_comap_uniformity := ⋯ },
      uniformity_dist := ⋯, toBornology := { cobounded := Filter.comap (⇑f) (Bornology.cobounded F), le_cofinite := ⋯ },
      cobounded_sets := ⋯, dist_eq := ⋯ }
-- Mathlib.Analysis.Complex.CanonicalDecomposition
Complex.canonicalFactor_apply_self : ∀ (R : ℝ) (w : ℂ), Complex.canonicalFactor R w w = 0
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
SimpleGraph.nonuniformWitnesses.congr_simp : ∀ {α : Type u_1} {𝕜 : Type u_2} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [inst_2 : IsStrictOrderedRing 𝕜]
  (G G_1 : SimpleGraph α),
  G = G_1 →
    ∀ {inst_3 : DecidableRel G.Adj} [inst_4 : DecidableRel G_1.Adj] (ε ε_1 : 𝕜),
      ε = ε_1 →
        ∀ (s s_1 : Finset α),
          s = s_1 → ∀ (t t_1 : Finset α), t = t_1 → G.nonuniformWitnesses ε s t = G_1.nonuniformWitnesses ε_1 s_1 t_1
-- Mathlib.Order.WithBot
WithTop.exists_le_coe : ∀ {α : Type u_1} {a : α} [inst : Preorder α] {p : WithTop α → Prop}, (∃ x ≤ ↑a, p x) ↔ ∃ b ≤ a, p ↑b
-- Mathlib.CategoryTheory.Monad.Products
CategoryTheory.coalgebraToOver_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : C) [inst_1 : CategoryTheory.Limits.HasBinaryProducts C]
  {X_1 Y : (CategoryTheory.prodComonad X).Coalgebra} (f : X_1 ⟶ Y),
  (CategoryTheory.coalgebraToOver X).map f = CategoryTheory.Over.homMk f.f ⋯
-- Mathlib.Analysis.Analytic.Composition
Composition.gather.eq_1 : ∀ {n : ℕ} (a : Composition n) (b : Composition a.length),
  a.gather b = { blocks := List.map List.sum (a.blocks.splitWrtComposition b), blocks_pos := ⋯, blocks_sum := ⋯ }
-- Mathlib.CategoryTheory.Idempotents.Biproducts
CategoryTheory.Idempotents.Karoubi.complement_p : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (P : CategoryTheory.Idempotents.Karoubi C), P.complement.p = CategoryTheory.CategoryStruct.id P.X - P.p
-- Mathlib.Topology.Compactness.LocallyCompact
IsLocallyClosed.locallyCompactSpace : ∀ {X : Type u_1} [inst : TopologicalSpace X] [LocallyCompactSpace X] {s : Set X},
  IsLocallyClosed s → LocallyCompactSpace ↑s