mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Compactness.CompactlyGeneratedSpace
/-- Every compactly generated space is a compactly coherent space.  -/
to_compactlyCoherentSpace : ∀ {X : Type u} [inst : TopologicalSpace X] [CompactlyGeneratedSpace X], CompactlyCoherentSpace X
-- Std.Time.Zoned.ZoneRules
Std.Time.TimeZone.ZoneRules.mk : Std.Time.TimeZone.LocalTimeType →
  Array Std.Time.TimeZone.Transition → Option Std.Time.TimeZone.RecurringRule → Std.Time.TimeZone.ZoneRules
-- Mathlib.Topology.Sets.Closeds
/-- the carrier set, i.e. the points in this set  -/
TopologicalSpace.IrreducibleCloseds.carrier : {α : Type u_4} → [inst : TopologicalSpace α] → TopologicalSpace.IrreducibleCloseds α → Set α
-- Mathlib.MeasureTheory.Function.LocallyIntegrable
ContinuousOn.integrableOn_uIcc : ∀ {X : Type u_1} {E : Type u_6} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] [inst_2 : NormedAddCommGroup E]
  {μ : MeasureTheory.Measure X} [OpensMeasurableSpace X] {f : X → E} {a b : X}
  [MeasureTheory.IsFiniteMeasureOnCompacts μ] [inst_5 : LinearOrder X] [CompactIccSpace X] [T2Space X],
  ContinuousOn f (Set.uIcc a b) → MeasureTheory.IntegrableOn f (Set.uIcc a b) μ
-- Mathlib.CategoryTheory.Limits.Fubini
/-- The colimit of `F.flip ⋙ colim` is isomorphic to the colimit of `F ⋙ colim`.  -/
CategoryTheory.Limits.colimitFlipCompColimIsoColimitCompColim : {J : Type u_1} →
  {K : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} J] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} K] →
        {C : Type u_3} →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} C] →
            (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) →
              [inst_3 : CategoryTheory.Limits.HasColimitsOfShape J C] →
                [inst_4 : CategoryTheory.Limits.HasColimitsOfShape K C] →
                  CategoryTheory.Limits.colimit (F.flip.comp CategoryTheory.Limits.colim) ≅
                    CategoryTheory.Limits.colimit (F.comp CategoryTheory.Limits.colim)
-- Mathlib.Algebra.Module.Congruence.Defs
VAddCon.instVAddQuotient : {S : Type u_2} → (M : Type u_3) → [inst : VAdd S M] → (c : VAddCon S M) → VAdd S (VAddCon.Quotient M c)
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
Nat.reduceGcd : Lean.Meta.Simp.DSimproc
-- Mathlib.RingTheory.Ideal.Maps
Ideal.comap_map_of_surjective : ∀ {R : Type u} {S : Type v} {F : Type u_1} [inst : Ring R] [inst_1 : Ring S] [inst_2 : FunLike F R S]
  [inst_3 : RingHomClass F R S] (f : F),
  Function.Surjective ⇑f → ∀ (I : Ideal R), Ideal.comap f (Ideal.map f I) = I ⊔ Ideal.comap f ⊥
-- Init.Data.BitVec.Lemmas
/-- The msb after arithmetic shifting right equals the original msb.  -/
BitVec.msb_sshiftRight : ∀ {w n : ℕ} {x : BitVec w}, (x.sshiftRight n).msb = x.msb
-- Mathlib.Order.Interval.Finset.SuccPred
Finset.Ioo_pred_left_eq_Ioc : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : LocallyFiniteOrder α] [inst_2 : PredOrder α] [NoMinOrder α] (a b : α),
  Finset.Ioo (Order.pred a) b = Finset.Ico a b
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
/-- `b < sSup s` when there is an element `a` in `s` with `b < a`, when `s` is bounded above.
This is essentially an iff, except that the assumptions for the two implications are
slightly different (one needs boundedness above for one direction, nonemptiness and linear
order for the other one), so we formulate separately the two implications, contrary to
the `CompleteLattice` case.  -/
lt_csSup_of_lt : ∀ {α : Type u_1} [inst : ConditionallyCompleteLattice α] {s : Set α} {a b : α}, BddAbove s → a ∈ s → b < a → b < sSup s
-- Mathlib.Topology.Algebra.ConstMulAction
instContinuousConstSMulForall : ∀ {M : Type u_1} {ι : Type u_4} {γ : ι → Type u_5} [inst : (i : ι) → TopologicalSpace (γ i)]
  [inst_1 : (i : ι) → SMul M (γ i)] [∀ (i : ι), ContinuousConstSMul M (γ i)], ContinuousConstSMul M ((i : ι) → γ i)
-- Lean.Elab.Tactic.Basic
Lean.Elab.Tactic.instMonadExceptExceptionTacticM : MonadExcept Lean.Exception Lean.Elab.Tactic.TacticM
-- Mathlib.Order.SuccPred.IntervalSucc
/-- If `α` is a linear pred order, `β` is a preorder, and `f : α → β` is a monotone function, then
the intervals `Set.Ico (f Order.pred n) (f n)` are pairwise disjoint.  -/
Monotone.pairwise_disjoint_on_Ico_pred : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : PredOrder α] [inst_2 : Preorder β] {f : α → β},
  Monotone f → Pairwise (Function.onFun Disjoint fun n => Set.Ico (f (Order.pred n)) (f n))
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.re_neg : ∀ {d : ℤ} (z : ℤ√d), (-z).re = -z.re
-- Mathlib.CategoryTheory.Monoidal.Closed.Basic
CategoryTheory.MonoidalClosed.closed : {C : Type u} →
  {inst : CategoryTheory.Category.{v, u} C} →
    {inst_1 : CategoryTheory.MonoidalCategory C} →
      [self : CategoryTheory.MonoidalClosed C] → (X : C) → CategoryTheory.Closed X
-- Mathlib.Order.Comparable
CompRel.of_compRel_of_antisymmRel : ∀ {α : Type u_1} {a b c : α} [inst : Preorder α],
  CompRel (fun x1 x2 => x1 ≤ x2) a b → AntisymmRel (fun x1 x2 => x1 ≤ x2) b c → CompRel (fun x1 x2 => x1 ≤ x2) a c
-- ProofWidgets.Component.Basic
ProofWidgets.MarkdownDisplay.instToJsonProps.toJson : ProofWidgets.MarkdownDisplay.Props → Lean.Json
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- **Alias** of `Topology.RelCWComplex.disjoint_skeletonLT_openCell`.

---

A skeleton and an open cell of a higher dimension are disjoint.  -/
Topology.CWComplex.disjoint_skeletonLT_openCell : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : T2Space X] [inst_1 : Topology.RelCWComplex C D] {n : ℕ∞}
  {m : ℕ} {j : Topology.RelCWComplex.cell C m},
  n ≤ ↑m → Disjoint (↑(Topology.RelCWComplex.skeletonLT C n)) (Topology.RelCWComplex.openCell m j)
-- Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
CategoryTheory.Abelian.SpectralObject.coreE₂HomologicalNat_i₃ : ∀ (r : ℤ) (pq : ℕ × ℕ) (hr : 2 ≤ r),
  CategoryTheory.Abelian.SpectralObject.coreE₂HomologicalNat.i₃ r pq hr = WithBotTop.coe (-↑pq.2 + r - 1)
-- Mathlib.RingTheory.Extension.Cotangent.Basis
_private.Mathlib.RingTheory.Extension.Cotangent.Basis.0.Algebra.Generators.PresentationOfFreeCotangent.Aux.instT : {R : Type u_1} →
  {S : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          {ι : Type u_4} →
            {P : Algebra.Generators R S ι} →
              {σ : Type u_5} →
                {b : Module.Basis σ S P.toExtension.Cotangent} →
                  (D : Algebra.Generators.PresentationOfFreeCotangent.Aux✝ P b) →
                    Algebra (Algebra.Generators.PresentationOfFreeCotangent.Aux.T✝ D) S
-- Init.Prelude
/-- The second element of a pair.  -/
Prod.snd : {α : Type u} → {β : Type v} → α × β → β
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.forIn'_roc : ∀ {α β : Type u} {m : Type u → Type v} {ps : Std.Do.PostShape} [inst : Monad m] [inst_1 : Std.Do.WPMonad m ps]
  [inst_2 : LE α] [inst_3 : DecidableLE α] [inst_4 : LT α] [inst_5 : Std.PRange.UpwardEnumerable α]
  [inst_6 : Std.Rxc.IsAlwaysFinite α] [inst_7 : Std.PRange.LawfulUpwardEnumerable α]
  [inst_8 : Std.PRange.LawfulUpwardEnumerableLE α] [inst_9 : Std.PRange.LawfulUpwardEnumerableLT α] {xs : Std.Roc α}
  {init : β} {f : (a : α) → a ∈ xs → β → m (ForInStep β)} (inv : Std.Do.Invariant xs.toList β ps),
  (∀ (pref : List α) (cur : α) (suff : List α) (h : xs.toList = pref ++ cur :: suff) (b : β),
      ⦃inv.1 ({ «prefix» := pref, suffix := cur :: suff, property := ⋯ }, b)⦄
        f cur ⋯ b ⦃(fun r =>
          match r with
          | ForInStep.yield b' => inv.1 ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
          | ForInStep.done b' => inv.1 ({ «prefix» := xs.toList, suffix := [], property := ⋯ }, b'),
          inv.2)⦄) →
    ⦃inv.1 ({ «prefix» := [], suffix := xs.toList, property := ⋯ }, init)⦄
      forIn' xs init f ⦃(fun b => inv.1 ({ «prefix» := xs.toList, suffix := [], property := ⋯ }, b), inv.2)⦄
-- Mathlib.Topology.MetricSpace.Cover
/-- **Alias** of the forward direction of `Metric.isCover_iff_subset_cthickening`. -/
Metric.IsCover.subset_cthickening : ∀ {X : Type u_1} [inst : PseudoMetricSpace X] {ε : NNReal} {s N : Set X} [ProperSpace X],
  IsClosed N → Metric.IsCover ε s N → s ⊆ Metric.cthickening (↑ε) N
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.Measure.IsAddHaarMeasure.comap : ∀ {G : Type u_1} {H : Type u_2} [inst : MeasurableSpace G] [inst_1 : MeasurableSpace H] [inst_2 : AddGroup G]
  [inst_3 : TopologicalSpace G] [BorelSpace G] [MeasurableAdd G] [inst_6 : AddGroup H] [inst_7 : TopologicalSpace H]
  [BorelSpace H] {mH : MeasurableAdd H} (μ : MeasureTheory.Measure H) [μ.IsAddHaarMeasure] {f : G →+ H},
  Topology.IsOpenEmbedding ⇑f → (MeasureTheory.Measure.comap (⇑f) μ).IsAddHaarMeasure
-- Mathlib.Data.NNReal.Star
instTrivialStarNNReal : TrivialStar NNReal
-- Mathlib.Topology.LocallyConstant.Basic
IsLocallyConstant.one : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : One Y], IsLocallyConstant 1
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
MeasureTheory.JordanDecomposition.instInvolutiveNeg : {α : Type u_1} → [inst : MeasurableSpace α] → InvolutiveNeg (MeasureTheory.JordanDecomposition α)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
cfc_ringInverse_id : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : Semifield R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : TopologicalSpace A] [inst_6 : Ring A]
  [inst_7 : StarRing A] [inst_8 : Algebra R A] [inst_9 : ContinuousFunctionalCalculus R A p] [ContinuousInv₀ R] (a : A),
  IsUnit a → autoParam (p a) cfc_ringInverse_id._auto_1 → cfc (fun x => x⁻¹) a = Ring.inverse a
-- Mathlib.RingTheory.Valuation.Basic
/-- A valuation gives a preorder on the underlying ring.  -/
AddValuation.toPreorder : {R : Type u_3} →
  {Γ₀ : Type u_4} → [inst : Ring R] → [inst_1 : LinearOrderedAddCommMonoidWithTop Γ₀] → AddValuation R Γ₀ → Preorder R
-- Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
HomotopicalAlgebra.BifibrantObject.instCongruenceHomRel : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C],
  CategoryTheory.Congruence (HomotopicalAlgebra.BifibrantObject.homRel C)
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.ULift
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.ULift.0.Std.IterM.length_eq_match_step.match_1.eq_3 : ∀ {α β : Type u_1} {m : Type u_1 → Type u_2} (motive : Std.IterStep (Std.IterM m β) β → Sort u_3)
  (h_1 : (it' : Std.IterM m β) → (out : β) → motive (Std.IterStep.yield it' out))
  (h_2 : (it' : Std.IterM m β) → motive (Std.IterStep.skip it')) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.done with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it' => h_2 it'
    | Std.IterStep.done => h_3 ()) =
    h_3 ()
-- Mathlib.Algebra.Group.AddChar
AddChar.add_apply : ∀ {A : Type u_2} {M : Type u_3} [inst : AddMonoid A] [inst_1 : CommMonoid M] (ψ φ : AddChar A M) (a : A),
  (ψ + φ) a = ψ a * φ a
-- Mathlib.LinearAlgebra.Matrix.Transvection
Matrix.toBlocks₁₂.eq_1 : ∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} (M : Matrix (n ⊕ o) (l ⊕ m) α),
  M.toBlocks₁₂ = Matrix.of fun i j => M (Sum.inl i) (Sum.inr j)
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
/-- A zero object is in particular initial.  -/
CategoryTheory.Limits.IsZero.isInitial : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X : C} → CategoryTheory.Limits.IsZero X → CategoryTheory.Limits.IsInitial X
-- Mathlib.RingTheory.MvPowerSeries.Substitution
MvPowerSeries.HasSubst.truncTotal : ∀ {σ : Type u_1} {τ : Type u_4} {S : Type u_5} [inst : CommRing S] {a : σ → MvPowerSeries τ S} {x : σ → ℕ}
  [inst_1 : Finite τ],
  MvPowerSeries.HasSubst a → MvPowerSeries.HasSubst fun i => ↑((MvPowerSeries.truncTotal (x i)) (a i))
-- Mathlib.Algebra.Ring.Subring.Defs
/-- A subring of a domain is a domain.  -/
SubringClass.instIsDomainSubtypeMem : ∀ {S : Type v} (s : S) {R : Type u_1} [inst : Ring R] [IsDomain R] [inst_2 : SetLike S R] [inst_3 : SubringClass S R],
  IsDomain ↥s
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.instMonoFKernelSequence : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C] {X Y : C}
  (f : X ⟶ Y), CategoryTheory.Mono (CategoryTheory.ShortComplex.kernelSequence f).f
-- Mathlib.Data.Matrix.Block
Matrix.blockDiagonal_transpose : ∀ {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} [inst : DecidableEq o] [inst_1 : Zero α]
  (M : o → Matrix m n α), (Matrix.blockDiagonal M).transpose = Matrix.blockDiagonal fun k => (M k).transpose
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.MonoidalCategory.tensorμ_natural : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {X₁ X₂ Y₁ Y₂ U₁ U₂ V₁ V₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (g₁ : U₁ ⟶ V₁)
  (g₂ : U₂ ⟶ V₂),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.tensorHom f₁ f₂)
        (CategoryTheory.MonoidalCategoryStruct.tensorHom g₁ g₂))
      (CategoryTheory.MonoidalCategory.tensorμ Y₁ Y₂ V₁ V₂) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ X₁ X₂ U₁ U₂)
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.tensorHom f₁ g₁)
        (CategoryTheory.MonoidalCategoryStruct.tensorHom f₂ g₂))
-- Mathlib.Tactic.Linter.UnusedInstancesInType
/-- The index of the binder that this instance came from. The first binder is `0`, and we do not
increment this index when seeing through `let`s.  -/
_private.Mathlib.Tactic.Linter.UnusedInstancesInType.0.Mathlib.Linter.UnusedInstancesInType.InstanceOfConcern.idx : Mathlib.Linter.UnusedInstancesInType.InstanceOfConcern✝ → ℕ
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.MonObj.instMonoOne : ∀ {D : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} D] [inst_1 : CategoryTheory.SemiCartesianMonoidalCategory D]
  (M : D) [inst_2 : CategoryTheory.MonObj M], CategoryTheory.Mono CategoryTheory.MonObj.one
-- Mathlib.Algebra.Lie.Weights.Cartan
LieAlgebra.zeroRootSubalgebra.congr_simp : ∀ (R : Type u_1) (L : Type u_2) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  (H H_1 : LieSubalgebra R L) (e_H : H = H_1) [inst_3 : LieRing.IsNilpotent ↥H],
  LieAlgebra.zeroRootSubalgebra R L H = LieAlgebra.zeroRootSubalgebra R L H_1
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.ConnectedComponent.ind : ∀ {V : Type u} {G : SimpleGraph V} {β : G.ConnectedComponent → Prop},
  (∀ (v : V), β (G.connectedComponentMk v)) → ∀ (c : G.ConnectedComponent), β c
-- Mathlib.CategoryTheory.Monoidal.Rigid.Basic
CategoryTheory.hasLeftDualUnit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      CategoryTheory.HasLeftDual (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
/-- Given a graded ring `A` and a map `f : A →+* Γ(X, ⊤)` such that the image of the
irrelevant ideal under `f` generates the whole ring, the set of `D(f(r))` for homogeneous `r`
of positive degree forms an open cover on `X`.  -/
AlgebraicGeometry.Proj.openCoverOfMapIrrelevantEqTop : {σ : Type u_1} →
  {A : Type u} →
    [inst : CommRing A] →
      [inst_1 : SetLike σ A] →
        [inst_2 : AddSubgroupClass σ A] →
          (𝒜 : ℕ → σ) →
            [inst_3 : GradedRing 𝒜] →
              {X : AlgebraicGeometry.Scheme} →
                (f : A →+* ↑(X.presheaf.obj (Opposite.op ⊤))) →
                  Ideal.map f (HomogeneousIdeal.irrelevant 𝒜).toIdeal = ⊤ → X.OpenCover
-- Mathlib.Order.Interval.Basic
Interval.coe_bot : ∀ {α : Type u_1} [inst : PartialOrder α], ↑⊥ = ∅
-- Mathlib.Data.ZMod.Defs
Fin.instPowNatOfNeZero_mathlib : (n : ℕ) → [NeZero n] → Pow (Fin n) ℕ
-- Mathlib.Tactic.Lemma
/-- `lemma` means the same as `theorem`. It is used to denote "less important" theorems  -/
lemma : Lean.ParserDescr
-- Mathlib.Order.Disjoint
codisjoint_inf_right : ∀ {α : Type u_1} [inst : DistribLattice α] [inst_1 : OrderTop α] {a b c : α},
  Codisjoint a (b ⊓ c) ↔ Codisjoint a b ∧ Codisjoint a c
-- Batteries.Data.HashMap.Basic
/-- Inserts key-value pair `a, b` into the map.
If an element equal to `a` is already in the map, it is replaced by `b`.
```
def hashMap := ofList [("one", 1), ("two", 2)]
hashMap.insert "three" 3 = {"one" => 1, "two" => 2, "three" => 3}
hashMap.insert "two" 0 = {"one" => 1, "two" => 0}
```
 -/
Batteries.HashMap.insert : {α : Type u_1} →
  {x : BEq α} → {x_1 : Hashable α} → {β : Type u_2} → Batteries.HashMap α β → α → β → Batteries.HashMap α β
-- Mathlib.Computability.EpsilonNFA
εNFA.εClosure_empty : ∀ {α : Type u} {σ : Type v} (M : εNFA α σ), M.εClosure ∅ = ∅
-- Init.Data.String.Lemmas.Order
String.Pos.next_ofSliceFrom : ∀ {s : String} {p₀ : s.Pos} {p : (s.sliceFrom p₀).Pos} {h : String.Pos.ofSliceFrom p ≠ s.endPos},
  (String.Pos.ofSliceFrom p).next h = String.Pos.ofSliceFrom (p.next ⋯)
-- Mathlib.LinearAlgebra.Span.Defs
Module.IsPrincipal.of_surjective : ∀ {R : Type u_1} {M : Type u_4} {M₂ : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M₂] (f : M →ₗ[R] M₂),
  Function.Surjective ⇑f → ∀ [Module.IsPrincipal R M], Module.IsPrincipal R M₂
-- Mathlib.GroupTheory.Commutator.Basic
Subgroup.commutator_top_left_eq_bot_iff_le_center : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G}, ⁅⊤, H⁆ = ⊥ ↔ H ≤ Subgroup.center G
-- Mathlib.Topology.UniformSpace.Basic
uniformity_multiplicative : ∀ {α : Type ua} [inst : UniformSpace α],
  uniformity (Multiplicative α) = Filter.map (Prod.map ⇑Multiplicative.ofAdd ⇑Multiplicative.ofAdd) (uniformity α)
-- Mathlib.Computability.TuringMachine.ToPartrec
_private.Mathlib.Computability.TuringMachine.ToPartrec.0.Turing.PartrecToTM2.trStmts₁.match_1.eq_2 : ∀ (motive : Turing.PartrecToTM2.Λ' → Sort u_1) (k : Turing.PartrecToTM2.K')
  (s : Option Turing.PartrecToTM2.Γ' → Option Turing.PartrecToTM2.Γ') (q : Turing.PartrecToTM2.Λ')
  (h_1 :
    (Q : Turing.PartrecToTM2.Λ') →
      (p : Turing.PartrecToTM2.Γ' → Bool) →
        (k₁ k₂ : Turing.PartrecToTM2.K') →
          (q : Turing.PartrecToTM2.Λ') →
            Q = Turing.PartrecToTM2.Λ'.move p k₁ k₂ q → motive (Turing.PartrecToTM2.Λ'.move p k₁ k₂ q))
  (h_2 :
    (Q : Turing.PartrecToTM2.Λ') →
      (k : Turing.PartrecToTM2.K') →
        (s : Option Turing.PartrecToTM2.Γ' → Option Turing.PartrecToTM2.Γ') →
          (q : Turing.PartrecToTM2.Λ') →
            Q = Turing.PartrecToTM2.Λ'.push k s q → motive (Turing.PartrecToTM2.Λ'.push k s q))
  (h_3 :
    (Q : Turing.PartrecToTM2.Λ') →
      (q : Option Turing.PartrecToTM2.Γ' → Turing.PartrecToTM2.Λ') →
        Q = Turing.PartrecToTM2.Λ'.read q → motive (Turing.PartrecToTM2.Λ'.read q))
  (h_4 :
    (Q : Turing.PartrecToTM2.Λ') →
      (p : Turing.PartrecToTM2.Γ' → Bool) →
        (k : Turing.PartrecToTM2.K') →
          (q : Turing.PartrecToTM2.Λ') →
            Q = Turing.PartrecToTM2.Λ'.clear p k q → motive (Turing.PartrecToTM2.Λ'.clear p k q))
  (h_5 : (Q q : Turing.PartrecToTM2.Λ') → Q = q.copy → motive q.copy)
  (h_6 : (Q q : Turing.PartrecToTM2.Λ') → Q = q.succ → motive q.succ)
  (h_7 : (Q q₁ q₂ : Turing.PartrecToTM2.Λ') → Q = q₁.pred q₂ → motive (q₁.pred q₂))
  (h_8 :
    (Q : Turing.PartrecToTM2.Λ') →
      (k : Turing.PartrecToTM2.Cont') → Q = Turing.PartrecToTM2.Λ'.ret k → motive (Turing.PartrecToTM2.Λ'.ret k)),
  (match Turing.PartrecToTM2.Λ'.push k s q with
    | Q@h:(Turing.PartrecToTM2.Λ'.move p k₁ k₂ q) => h_1 Q p k₁ k₂ q h
    | Q@h:(Turing.PartrecToTM2.Λ'.push k s q) => h_2 Q k s q h
    | Q@h:(Turing.PartrecToTM2.Λ'.read q) => h_3 Q q h
    | Q@h:(Turing.PartrecToTM2.Λ'.clear p k q) => h_4 Q p k q h
    | Q@h:q.copy => h_5 Q q h
    | Q@h:q.succ => h_6 Q q h
    | Q@h:(q₁.pred q₂) => h_7 Q q₁ q₂ h
    | Q@h:(Turing.PartrecToTM2.Λ'.ret k) => h_8 Q k h) =
    h_2 (Turing.PartrecToTM2.Λ'.push k s q) k s q ⋯
-- Mathlib.Algebra.Group.Defs
LeftCancelSemigroup.ext_iff : ∀ {G : Type u} {x y : LeftCancelSemigroup G}, x = y ↔ Mul.mul = Mul.mul
-- Lean.DocString.Parser
/-- Parses a role.  -/
Lean.Doc.Parser.role : Lean.Doc.Parser.InlineCtxt → Lean.Parser.ParserFn
-- Mathlib.Algebra.Group.Semiconj.Basic
/-- **Alias** of the reverse direction of `AddSemiconjBy.neg_neg_symm_iff`. -/
AddSemiconjBy.neg_neg_symm : ∀ {G : Type u_1} [inst : SubtractionMonoid G] {a x y : G}, AddSemiconjBy a y x → AddSemiconjBy (-a) (-x) (-y)
-- Mathlib.Topology.CompactOpen
ContinuousMap.instT0Space : ∀ {X : Type u_2} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [T0Space Y], T0Space C(X, Y)
-- Mathlib.MeasureTheory.VectorMeasure.Integral
/-- **Lebesgue dominated convergence theorem** provides sufficient conditions under which almost
everywhere convergence of a sequence of functions implies the convergence of their integrals.
We could weaken the condition `bound_integrable` to require
`HasFiniteIntegral bound μ.variation` instead (i.e. not requiring that `bound` is
measurable), but in all applications proving integrability is easier.  -/
MeasureTheory.VectorMeasure.tendsto_integral_of_dominated_convergence : ∀ {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G]
  [inst_5 : NormedSpace ℝ G] {μ : MeasureTheory.VectorMeasure X F} {B : E →L[ℝ] F →L[ℝ] G} {F_1 : ℕ → X → E} {f : X → E}
  (bound : X → ℝ),
  (∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (F_1 n) μ.variation) →
    MeasureTheory.Integrable bound μ.variation →
      (∀ (n : ℕ), ∀ᵐ (a : X) ∂μ.variation, ‖F_1 n a‖ ≤ bound a) →
        (∀ᵐ (a : X) ∂μ.variation, Filter.Tendsto (fun n => F_1 n a) Filter.atTop (nhds (f a))) →
          Filter.Tendsto (fun n => ∫ᵛ (a : X), F_1 n a ∂[B; μ]) Filter.atTop (nhds ∫ᵛ (a : X), f a ∂[B; μ])
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.sdiff_nonempty_of_mk_lt_mk : ∀ {α : Type u} {S T : Set α}, Cardinal.mk ↑S < Cardinal.mk ↑T → (T \ S).Nonempty
-- Mathlib.Topology.Algebra.Group.Basic
Homeomorph.neg.eq_1 : ∀ (G : Type u_1) [inst : TopologicalSpace G] [inst_1 : InvolutiveNeg G] [inst_2 : ContinuousNeg G],
  Homeomorph.neg G = { toEquiv := Equiv.neg G, continuous_toFun := ⋯, continuous_invFun := ⋯ }
-- Mathlib.CategoryTheory.InducedCategory
/-- Morphisms in `InducedCategory D F` identify to morphisms in `D`.  -/
CategoryTheory.InducedCategory.homEquiv : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v, u₂} D] →
      {F : C → D} → {X Y : CategoryTheory.InducedCategory D F} → (X ⟶ Y) ≃ (F X ⟶ F Y)
-- Lean.Elab.Tactic.SimpTrace
/-- Filter out `+suggestions` and `+locals` from the config syntax  -/
Lean.Elab.Tactic.filterSuggestionsAndLocalsFromSimpConfig : Lean.TSyntax `Lean.Parser.Tactic.optConfig → Lean.MetaM (Lean.TSyntax `Lean.Parser.Tactic.optConfig)
-- Mathlib.Algebra.Module.LinearMap.Basic
LinearMap.instDistribMulActionDomMulActOfSMulCommClass : {R : Type u_1} →
  {R' : Type u_2} →
    {M : Type u_4} →
      {M' : Type u_5} →
        [inst : Semiring R] →
          [inst_1 : Semiring R'] →
            [inst_2 : AddCommMonoid M] →
              [inst_3 : AddCommMonoid M'] →
                [inst_4 : Module R M] →
                  [inst_5 : Module R' M'] →
                    {σ₁₂ : R →+* R'} →
                      {S' : Type u_6} →
                        [inst_6 : Monoid S'] →
                          [inst_7 : DistribMulAction S' M] →
                            [SMulCommClass R S' M] → DistribMulAction S'ᵈᵐᵃ (M →ₛₗ[σ₁₂] M')
-- Mathlib.Algebra.Order.Monoid.Unbundled.Units
/-- **Alias** of the forward direction of `Units.le_mul_inv_iff`. -/
Units.mul_le_of_le_mul_inv : ∀ {M : Type u_1} [inst : Monoid M] [inst_1 : LE M] [MulRightMono M] {a b : M} (u : Mˣ), a ≤ b * ↑u⁻¹ → a * ↑u ≤ b