mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.NumberTheory.Transcendental.Liouville.Measure
setOfPred_liouvilleWith_subset_aux : {x | ∃ p > 2, LiouvilleWith p x} ⊆
  ⋃ m,
    (fun x => x + ↑m) ⁻¹'
      ⋃ n, ⋃ (_ : n > 0), {x | ∃ᶠ (b : ℕ) in Filter.atTop, ∃ a ∈ Finset.Icc 0 ↑b, |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑n)}
-- Init.Data.String.Lemmas.Splits
String.copy_slice_eq_iff_splits : ∀ {t s : String} {pos₁ pos₂ : s.Pos},
  (∃ (h : pos₁ ≤ pos₂), (s.slice pos₁ pos₂ h).copy = t) ↔ ∃ t₁ t₂, pos₁.Splits t₁ (t ++ t₂) ∧ pos₂.Splits (t₁ ++ t) t₂
-- Mathlib.CategoryTheory.Triangulated.Triangulated
CategoryTheory.Triangulated.Octahedron.triangleMorphism₂_hom₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃}
  {comm : CategoryTheory.CategoryStruct.comp u₁₂ u₂₃ = u₁₃} {v₁₂ : X₂ ⟶ Z₁₂}
  {w₁₂ : Z₁₂ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁}
  {h₁₂ : CategoryTheory.Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  {v₂₃ : X₃ ⟶ Z₂₃} {w₂₃ : Z₂₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₂}
  {h₂₃ : CategoryTheory.Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  {v₁₃ : X₃ ⟶ Z₁₃} {w₁₃ : Z₁₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁}
  {h₁₃ : CategoryTheory.Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  (h : CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃), h.triangleMorphism₂.hom₁ = u₁₂
-- Mathlib.RepresentationTheory.Tannaka
TannakaDuality.FiniteGroup.equivHom_surjective : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] [Finite G] [IsDomain k],
  Function.Surjective ⇑(TannakaDuality.FiniteGroup.equivHom k G)
-- Lean.Meta.Tactic.Grind.Types
_private.Lean.Meta.Tactic.Grind.Types.0.Lean.Meta.Grind.MethodsRef.toMethods.unsafe_1 : Lean.Meta.Grind.MethodsRef → Lean.Meta.Grind.Methods
-- Mathlib.Topology.Defs.Induced
WithTopology.topology_eq_coinduced : ∀ (X : Type u_1) (t : TopologicalSpace X),
  WithTopology.instTopologicalSpace X t = TopologicalSpace.coinduced (WithTopology.toTopology t) t
-- Mathlib.Tactic.Sat.FromLRAT
/-- The reification of the empty clause is `True`: `¬⟦⊥⟧_v ≡ True`.  -/
Sat.Clause.reify_zero : ∀ {v : Sat.Valuation}, Sat.Clause.reify v Sat.Clause.nil True
-- Mathlib.GroupTheory.GroupAction.Hom
MulActionHom.instCommRing : {M : Type u_2} →
  {N : Type u_3} →
    {X : Type u_4} →
      {Y : Type u_5} →
        {σ : M → N} →
          [inst : SMul M X] →
            [inst_1 : Monoid N] → [inst_2 : CommRing Y] → [inst_3 : MulSemiringAction N Y] → CommRing (X →ₑ[σ] Y)
-- Mathlib.Algebra.GroupWithZero.NonZeroDivisors
isUnit_of_mem_nonZeroDivisors : ∀ {G₀ : Type u_1} [inst : GroupWithZero G₀] {x : G₀}, x ∈ nonZeroDivisors G₀ → IsUnit x
-- Mathlib.Algebra.Ring.Hom.Defs
/-- The proposition that the function preserves addition  -/
NonUnitalRingHom.map_add' : ∀ {α : Type u_5} {β : Type u_6} [inst : NonUnitalNonAssocSemiring α] [inst_1 : NonUnitalNonAssocSemiring β]
  (self : α →ₙ+* β) (x y : α), self.toFun (x + y) = self.toFun x + self.toFun y
-- Lean.ScopedEnvExtension
Lean.ScopedEnvExtension.modifyState : {α β σ : Type} → Lean.ScopedEnvExtension α β σ → Lean.Environment → (σ → σ) → Lean.Environment
-- Mathlib.CategoryTheory.Triangulated.Basic
/-- A morphism of triangles `(X,Y,Z,f,g,h) ⟶ (X',Y',Z',f',g',h')` in `C` is a triple of morphisms
`a : X ⟶ X'`, `b : Y ⟶ Y'`, `c : Z ⟶ Z'` such that
`a ≫ f' = f ≫ b`, `b ≫ g' = g ≫ c`, and `a⟦1⟧' ≫ h = h' ≫ c`.
In other words, we have a commutative diagram:
```
     f      g      h
  X  ───> Y  ───> Z  ───> X⟦1⟧
  │       │       │        │
  │a      │b      │c       │a⟦1⟧'
  V       V       V        V
  X' ───> Y' ───> Z' ───> X'⟦1⟧
     f'     g'     h'
```
 -/
CategoryTheory.Pretriangulated.TriangleMorphism : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.HasShift C ℤ] →
      CategoryTheory.Pretriangulated.Triangle C → CategoryTheory.Pretriangulated.Triangle C → Type v
-- Mathlib.Data.Prod.PProd
PProd.forall : ∀ {α : Sort u_1} {β : Sort u_2} {p : α ×' β → Prop}, (∀ (x : α ×' β), p x) ↔ ∀ (a : α) (b : β), p ⟨a, b⟩
-- Mathlib.Topology.Sets.CompactOpenCovered
IsCompactOpenCovered.iff_isCompactOpenCovered_sigmaMk : ∀ {S : Type u_1} {ι : Type u_2} {X : ι → Type u_3} {f : (i : ι) → X i → S} [inst : (i : ι) → TopologicalSpace (X i)]
  {U : Set S}, IsCompactOpenCovered f U ↔ IsCompactOpenCovered (fun x p => f p.fst p.snd) U
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.mem_filter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp] {f : α → β → Bool}
  {k : α}, t.WF → (k ∈ Std.TreeMap.Raw.filter f t ↔ ∃ (h' : k ∈ t), f (t.getKey k h') t[k] = true)
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
/-- Evaluate ` (α ≫ η ≫ ηs) ▷ j`  -/
Mathlib.Tactic.BicategoryLike.MkEvalWhiskerRight.mkEvalWhiskerRightConsOfOf : {m : Type → Type} →
  [self : Mathlib.Tactic.BicategoryLike.MkEvalWhiskerRight m] →
    Mathlib.Tactic.BicategoryLike.Atom₁ →
      Mathlib.Tactic.BicategoryLike.Structural →
        Mathlib.Tactic.BicategoryLike.HorizontalComp →
          Mathlib.Tactic.BicategoryLike.NormalExpr →
            Mathlib.Tactic.BicategoryLike.NormalExpr →
              Mathlib.Tactic.BicategoryLike.NormalExpr →
                Mathlib.Tactic.BicategoryLike.NormalExpr →
                  Mathlib.Tactic.BicategoryLike.NormalExpr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → m Lean.Expr
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.shortComplex_X₁ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.shortComplex._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.shortComplex._auto_3),
  (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).X₁ = (X.H n₀).obj (CategoryTheory.ComposableArrows.mk₁ f₃)
-- Mathlib.Topology.MetricSpace.CoveringNumbers
Metric.IsCover.coveringNumber_le_encard : ∀ {X : Type u_1} [inst : PseudoEMetricSpace X] {A C : Set X} {ε : NNReal},
  C ⊆ A → Metric.IsCover ε A C → Metric.coveringNumber ε A ≤ C.encard
-- Init.Core
iff_true_intro : ∀ {a : Prop}, a → (a ↔ True)
-- Mathlib.Topology.Semicontinuity.Basic
/-- **Alias** of the reverse direction of `upperSemicontinuousOn_neg_iff`. -/
LowerSemicontinuousOn.neg : ∀ {α : Type u_4} [inst : TopologicalSpace α] {β : Type u_5} {f : α → β} {s : Set α} [inst_1 : PartialOrder β]
  [inst_2 : AddCommGroup β] [IsOrderedAddMonoid β], LowerSemicontinuousOn f s → UpperSemicontinuousOn (-f) s
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
/-- Constructing a linear map `(⨂[R] i, s i) → E` given a `MultilinearMap R s E` with the
property that its composition with the canonical `MultilinearMap R s E` is
the given multilinear map `φ`.  -/
PiTensorProduct.lift : {ι : Type u_1} →
  {R : Type u_4} →
    [inst : CommSemiring R] →
      {s : ι → Type u_7} →
        [inst_1 : (i : ι) → AddCommMonoid (s i)] →
          [inst_2 : (i : ι) → Module R (s i)] →
            {E : Type u_9} →
              [inst_3 : AddCommMonoid E] →
                [inst_4 : Module R E] → MultilinearMap R s E ≃ₗ[R] (PiTensorProduct R fun i => s i) →ₗ[R] E
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.nnnorm_toLp : ∀ {ι : Type u_2} {β : ι → Type u_4} [inst : Fintype ι] [inst_1 : (i : ι) → SeminormedAddCommGroup (β i)]
  (f : (i : ι) → β i), ‖WithLp.toLp ⊤ f‖₊ = ‖f‖₊
-- Mathlib.Combinatorics.Matroid.Map
Matroid.mapEquiv_ground_eq : ∀ {α : Type u_1} {β : Type u_2} (M : Matroid α) (f : α ≃ β), (M.mapEquiv f).E = ⇑f '' M.E
-- Mathlib.RingTheory.MvPowerSeries.Evaluation
MvPowerSeries.coe_hasEvalIdeal : ∀ {σ : Type u_1} {S : Type u_3} [inst : CommRing S] [inst_1 : TopologicalSpace S] [inst_2 : IsTopologicalRing S]
  [inst_3 : IsLinearTopology S S], ↑MvPowerSeries.hasEvalIdeal = {a | MvPowerSeries.HasEval a}
-- Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt
SummationFilter.hasProd_symmetricIco_int_iff : ∀ {α : Type u_2} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] {f : ℤ → α} {a : α},
  HasProd f a (SummationFilter.symmetricIco ℤ) ↔
    Filter.Tendsto (fun N => ∏ n ∈ Finset.Ico (-↑N) ↑N, f n) Filter.atTop (nhds a)
-- Mathlib.Analysis.Normed.Group.Defs
NormedCommGroup.toSeminormedCommGroup.eq_1 : ∀ {E : Type u_5} [inst : NormedCommGroup E],
  NormedCommGroup.toSeminormedCommGroup =
    { toNorm := inst.toNorm, toCommGroup := inst.toCommGroup, toPseudoMetricSpace := inst.toPseudoMetricSpace,
      dist_eq := ⋯ }
-- Mathlib.LinearAlgebra.Contraction
dualTensorHom_finsupp_bijective : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N],
  Finite ι ∨ Module.Finite R M →
    Function.Bijective ⇑(dualTensorHom R M N) → Function.Bijective ⇑(dualTensorHom R M (ι →₀ N))
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.sum_biUnion_of_pairwise_eq_zero : ∀ {ι : Type u_1} {κ : Type u_2} {M : Type u_4} [inst : AddCommMonoid M] {f : ι → M} [inst_1 : DecidableEq ι]
  {s : Finset κ} {t : κ → Finset ι},
  ((↑s).Pairwise fun i j => ∀ k ∈ t i ∩ t j, f k = 0) → ∑ x ∈ s.biUnion t, f x = ∑ x ∈ s, ∑ i ∈ t x, f i
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.comap_comap : ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : MulOneClass M] [inst_1 : MulOneClass N] [inst_2 : MulOneClass P]
  (S : Submonoid P) (g : N →* P) (f : M →* N), Submonoid.comap f (Submonoid.comap g S) = Submonoid.comap (g.comp f) S
-- Mathlib.Probability.Martingale.Upcrossing
MeasureTheory.lowerCrossingTime_mono : ∀ {Ω : Type u_1} {ι : Type u_2} [inst : ConditionallyCompleteLinearOrderBot ι] {a b : ℝ} {f : ι → Ω → ℝ} {N : ι}
  {n m : ℕ} {ω : Ω}, n ≤ m → MeasureTheory.lowerCrossingTime a b f N n ω ≤ MeasureTheory.lowerCrossingTime a b f N m ω
-- Init.Data.List.MapIdx
/-- Auxiliary for `mapFinIdxM`:
`mapFinIdxM.go [a₀, a₁, ...] acc = acc.toList ++ [f 0 a₀ ⋯, f 1 a₁ ⋯, ...]`  -/
List.mapFinIdxM.go : {m : Type u_1 → Type u_2} →
  {α : Type u_3} →
    {β : Type u_1} →
      [Monad m] →
        (as : List α) →
          ((i : ℕ) → α → i < as.length → m β) →
            (bs : List α) → (acc : Array β) → bs.length + acc.size = as.length → m (List β)
-- Aesop.Script.Tactic
Aesop.Script.Tactic.mk : Aesop.Script.UTactic → Option Aesop.Script.STactic → Aesop.Script.Tactic
-- Mathlib.CategoryTheory.ComposableArrows.Two
/-- The morphism `mk₁ f ⟶ mk₁ fg` when `f ≫ g = fg` for some morphism `g`.  -/
CategoryTheory.ComposableArrows.twoδ₂Toδ₁ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {i j k : C} →
      (f : i ⟶ j) →
        (g : j ⟶ k) →
          (fg : i ⟶ k) →
            autoParam (CategoryTheory.CategoryStruct.comp f g = fg) CategoryTheory.ComposableArrows.twoδ₂Toδ₁._auto_1 →
              (CategoryTheory.ComposableArrows.mk₁ f ⟶ CategoryTheory.ComposableArrows.mk₁ fg)
-- Mathlib.Analysis.Complex.Convex
Complex.instPathConnectedSpaceUnits : PathConnectedSpace ℂˣ
-- Mathlib.GroupTheory.GroupAction.Quotient
AddAction.right_quotientAction : ∀ {G : Type u} [inst : AddGroup G] (H : AddSubgroup G), AddAction.QuotientAction (↥(AddSubgroup.normalizer ↑H).op) H
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.throw_OptionT : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {α : Type u} {e : PUnit.{u + 1}}
  {Q : Std.Do.PostCond α (Std.Do.PostShape.except PUnit.{u + 1} ps)} [inst : Monad m] [inst_1 : Std.Do.WPMonad m ps],
  ⦃Q.2.1 e⦄ MonadExceptOf.throw e ⦃Q⦄
-- Mathlib.Analysis.Convex.Jensen
/-- Convex **Jensen's inequality** where an element plays a distinguished role.  -/
ConvexOn.map_add_sum_le : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} {ι : Type u_5} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜]
  [IsStrictOrderedRing 𝕜] [inst_3 : AddCommGroup E] [inst_4 : AddCommGroup β] [inst_5 : PartialOrder β]
  [IsOrderedAddMonoid β] [inst_7 : Module 𝕜 E] [inst_8 : Module 𝕜 β] [IsStrictOrderedModule 𝕜 β] {s : Set E} {f : E → β}
  {t : Finset ι} {w : ι → 𝕜} {p : ι → E} {v : 𝕜} {q : E},
  ConvexOn 𝕜 s f →
    (∀ i ∈ t, 0 ≤ w i) →
      v + ∑ i ∈ t, w i = 1 →
        (∀ i ∈ t, p i ∈ s) → 0 ≤ v → q ∈ s → f (v • q + ∑ i ∈ t, w i • p i) ≤ v • f q + ∑ i ∈ t, w i • f (p i)
-- Mathlib.Algebra.Category.CommBialgCat
CommBialgCat.id_apply : ∀ {R : Type u} [inst : CommRing R] (A : CommBialgCat R) (a : ↑A),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id A)) a = a
-- Mathlib.LinearAlgebra.Matrix.Bilinear
mulLinearMap_apply_apply : ∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} (R : Type u_5) {A : Type u_6} [inst : Fintype m]
  [inst_1 : CommSemiring R] [inst_2 : NonUnitalNonAssocSemiring A] [inst_3 : Module R A] [inst_4 : SMulCommClass R A A]
  [inst_5 : IsScalarTower R A A] (X : Matrix l m A) (x : Matrix m n A), ((mulLinearMap R) X) x = X * x
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.Std.DHashMap.Internal.AssocList.foldr.eq_1 : ∀ {α : Type u} {β : α → Type v} {δ : Type w} (f : (a : α) → β a → δ → δ) (init : δ)
  (as : Std.DHashMap.Internal.AssocList α β),
  Std.DHashMap.Internal.AssocList.foldr f init as =
    (Std.DHashMap.Internal.AssocList.foldrM (fun x1 x2 x3 => pure (f x1 x2 x3)) init as).run
-- Mathlib.Algebra.Star.SelfAdjoint
IsStarNormal.val_inv : ∀ {R : Type u_1} [inst : Monoid R] [inst_1 : StarMul R] {x : Rˣ} [IsStarNormal ↑x], IsStarNormal ↑x⁻¹
-- Mathlib.Algebra.Category.ModuleCat.Semi
LinearMap.id_semiModuleCat_comp : ∀ {R : Type u_1} [inst : Semiring R] {G : Type u} [inst_1 : AddCommMonoid G] [inst_2 : Module R G] {H : SemimoduleCat R}
  (f : G →ₗ[R] ↑H), SemimoduleCat.Hom.hom (CategoryTheory.CategoryStruct.id H) ∘ₗ f = f
-- Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor
CategoryTheory.Functor.RightLinear.δᵣ_comp_μᵣ : ∀ {D : Type u_1} {D' : Type u_2} {inst : CategoryTheory.Category.{v_1, u_1} D}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} D'} (F : CategoryTheory.Functor D D') {C : Type u_3}
  {inst_2 : CategoryTheory.Category.{v_3, u_3} C} {inst_3 : CategoryTheory.MonoidalCategory C}
  {inst_4 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D}
  {inst_5 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D'} [self : F.RightLinear C] (d : D) (c : C),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxRightLinear.δᵣ F d c)
      (CategoryTheory.Functor.LaxRightLinear.μᵣ F d c) =
    CategoryTheory.CategoryStruct.id (F.obj (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj d c))
-- Init.Control.Id
Id.instMonadAttach : MonadAttach Id
-- Mathlib.Algebra.Group.Subgroup.Pointwise
/-- Applying a `MulDistribMulAction` results in an isomorphic subgroup  -/
Subgroup.equivSMul : {α : Type u_1} →
  {G : Type u_2} →
    [inst : Group G] →
      [inst_1 : Group α] → [inst_2 : MulDistribMulAction α G] → (a : α) → (H : Subgroup G) → ↥H ≃* ↥(a • H)
-- Init.Data.Range.Polymorphic.UInt
USize.instHasSize_1 : Std.Rxo.HasSize USize
-- Mathlib.FieldTheory.IntermediateField.Basic
/-- The action by an intermediate field is the action by the underlying field.  -/
IntermediateField.instMulActionWithZeroSubtypeMem : {K : Type u_1} →
  {L : Type u_2} →
    [inst : Field K] →
      [inst_1 : Field L] →
        [inst_2 : Algebra K L] →
          {X : Type u_4} →
            [inst_3 : Zero X] → [MulActionWithZero L X] → (F : IntermediateField K L) → MulActionWithZero (↥F) X
-- Init.Grind.Order
Lean.Grind.Order.le_eq_true : ∀ {α : Type u_1} [inst : LE α] [Std.IsPreorder α] {a : α}, (a ≤ a) = True
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.id_h₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreOneHypercover S) {i j : E.I₀}
  (x : E.I₁ i j), (CategoryTheory.CategoryStruct.id E).h₁ x = CategoryTheory.CategoryStruct.id (E.Y x)
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.CompactOpens.coe_toOpens : ∀ {α : Type u_1} [inst : TopologicalSpace α] (s : TopologicalSpace.CompactOpens α), ↑s.toOpens = ↑s
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.eLpNorm'_const' : ∀ {α : Type u_1} {F : Type u_5} {m0 : MeasurableSpace α} {q : ℝ} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup F] [MeasureTheory.IsFiniteMeasure μ] (c : F),
  c ≠ 0 → q ≠ 0 → MeasureTheory.eLpNorm' (fun x => c) q μ = ‖c‖ₑ * μ Set.univ ^ (1 / q)
-- Mathlib.Algebra.WithConv
WithConv.ofConv_listSum : ∀ {A : Type u_2} [inst : AddCommMonoid A] (l : List (WithConv A)), l.sum.ofConv = (List.map WithConv.ofConv l).sum
-- Mathlib.Algebra.Opposites
MulOpposite.instIsCancelAdd : ∀ {α : Type u_1} [inst : Add α] [IsCancelAdd α], IsCancelAdd αᵐᵒᵖ
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.eq_d₁₂_comp_inv : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G),
  CategoryTheory.CategoryStruct.comp (groupCohomology.cochainsIso₁ A).inv
      ((groupCohomology.inhomogeneousCochains A).d 1 2) =
    CategoryTheory.CategoryStruct.comp (groupCohomology.d₁₂ A) (groupCohomology.cochainsIso₂ A).inv
-- Lean.Data.Lsp.Basic
Lean.Lsp.CreateFile : Type
-- Init.Data.BitVec.Lemmas
/-- When `r < w`, we give a formula for `(x.rotateRight r).getLsb i`.  -/
BitVec.getLsbD_rotateRight_of_lt : ∀ {w : ℕ} {x : BitVec w} {r i : ℕ},
  r < w →
    (x.rotateRight r).getLsbD i =
      bif decide (i < w - r) then x.getLsbD (r + i) else decide (i < w) && x.getLsbD (i - (w - r))
-- Mathlib.Analysis.ODE.PicardLindelof
/-- The time interval of validity  -/
IsPicardLindelof.mul_max_le : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {f : ℝ → E → E} {tmin tmax : ℝ} {t₀ : ↑(Set.Icc tmin tmax)} {x₀ : E}
  {a r L K : NNReal}, IsPicardLindelof f t₀ x₀ a r L K → ↑L * max (tmax - ↑t₀) (↑t₀ - tmin) ≤ ↑a - ↑r
-- Mathlib.RingTheory.Coalgebra.CoassocSimps
CoassocSimps.assoc_symm_comp_map_assoc : ∀ {R : Type u_1} {M : Type u_3} {P : Type u_5} {M₁ : Type u_11} {M₂ : Type u_12} {M₃ : Type u_13} {N₁ : Type u_14}
  [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [inst_3 : AddCommMonoid P]
  [inst_4 : Module R P] [inst_5 : AddCommMonoid M₁] [inst_6 : AddCommMonoid M₂] [inst_7 : AddCommMonoid M₃]
  [inst_8 : AddCommMonoid N₁] [inst_9 : Module R M₁] [inst_10 : Module R M₂] [inst_11 : Module R M₃]
  [inst_12 : Module R N₁] (f₁ : M₁ →ₗ[R] N₁) (f₂₃ : M →ₗ[R] TensorProduct R M₂ M₃) (f : P →ₗ[R] TensorProduct R M₁ M),
  ↑(TensorProduct.assoc R N₁ M₂ M₃).symm ∘ₗ TensorProduct.map f₁ f₂₃ ∘ₗ f =
    TensorProduct.map (TensorProduct.map f₁ LinearMap.id) LinearMap.id ∘ₗ
      ↑(TensorProduct.assoc R M₁ M₂ M₃).symm ∘ₗ TensorProduct.map LinearMap.id f₂₃ ∘ₗ f
-- Init.Core
false_ne_true : False ≠ True
-- Mathlib.Algebra.Order.Hom.MonoidWithZero
OrderMonoidWithZeroHom.instFunLike : {α : Type u_2} →
  {β : Type u_3} →
    [inst : Preorder α] →
      [inst_1 : Preorder β] → [inst_2 : MulZeroOneClass α] → [inst_3 : MulZeroOneClass β] → FunLike (α →*₀o β) α β
-- Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
/-- `reverse` is a no-op over `CliffordAlgebraComplex.Q`.  -/
CliffordAlgebraComplex.reverse_apply : ∀ (x : CliffordAlgebra CliffordAlgebraComplex.Q), CliffordAlgebra.reverse x = x
-- Init.Data.List.Nat.Basic
_private.Init.Data.List.Nat.Basic.0.List.filterMap.match_1.splitter : {β : Type u_1} →
  (motive : Option β → Sort u_2) → (x : Option β) → (Unit → motive none) → ((b : β) → motive (some b)) → motive x
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get_congr : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β}
  [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] (h : m.WF) {a b : α} (hab : (a == b) = true) {h' : a ∈ m},
  Std.DHashMap.Raw.Const.get m a h' = Std.DHashMap.Raw.Const.get m b ⋯
-- Mathlib.Topology.Order.LeftRight
nhdsGE_neBot : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : Preorder α] (a : α), (nhdsWithin a (Set.Ici a)).NeBot
-- Mathlib.Data.Set.Order
StrictAntiOn.eq_1 : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] (f : α → β) (s : Set α),
  StrictAntiOn f s = ∀ ⦃a : α⦄, a ∈ s → ∀ ⦃b : α⦄, b ∈ s → a < b → f b < f a
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.ofCoeff.inj : ∀ {k : Type u_1} {G : Type u_2} {inst : Zero k} {coeff coeff_1 : G →₀ k},
  { coeff := coeff } = { coeff := coeff_1 } → coeff = coeff_1
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Algebra.commute_of_mem_adjoin_of_forall_mem_commute : ∀ {R : Type uR} {A : Type uA} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] {a b : A}
  {s : Set A}, b ∈ Algebra.adjoin R s → (∀ b ∈ s, Commute a b) → Commute a b
-- Mathlib.NumberTheory.FLT.Four
/-- if we have a solution to `a ^ 4 + b ^ 4 = c ^ 2` then there must be a minimal one.  -/
Fermat42.exists_minimal : ∀ {a b c : ℤ}, Fermat42 a b c → ∃ a0 b0 c0, Fermat42.Minimal a0 b0 c0
-- Mathlib.Order.Filter.IsBounded
Monotone.isCoboundedUnder_ge_of_isCobounded : ∀ {R : Type u_5} {S : Type u_6} {F : Filter R} [inst : LinearOrder R] [inst_1 : LinearOrder S] {f : R → S},
  Monotone f →
    ∀ [F.NeBot], Filter.IsCobounded (fun x1 x2 => x2 ≤ x1) F → Filter.IsCoboundedUnder (fun x1 x2 => x2 ≤ x1) F f
-- Mathlib.Algebra.Category.BialgCat.Basic
BialgCat.instBialgebra : {R : Type u} → [inst : CommRing R] → (self : BialgCat R) → Bialgebra R self.carrier
-- Mathlib.Analysis.Polynomial.Basic
Polynomial.isEquivalent_atTop_lead : ∀ {𝕜 : Type u_1} [inst : NormedField 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (P : Polynomial 𝕜)
  [OrderTopology 𝕜],
  Asymptotics.IsEquivalent Filter.atTop (fun x => Polynomial.eval x P) fun x => P.leadingCoeff * x ^ P.natDegree
-- Mathlib.Algebra.Polynomial.Mirror
Polynomial.mirror_mul_of_domain : ∀ {R : Type u_1} [inst : Semiring R] (p q : Polynomial R) [NoZeroDivisors R], (p * q).mirror = p.mirror * q.mirror
-- Std.Data.Internal.List.Associative
Std.Internal.List.minKey_of_perm : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {l l' : List ((a : α) × β a)} {hl : l.isEmpty = false},
  Std.Internal.List.DistinctKeys l → ∀ (hp : l.Perm l'), Std.Internal.List.minKey l hl = Std.Internal.List.minKey l' ⋯
-- Mathlib.Algebra.FreeMonoid.Basic
FreeMonoid.freeMonoidCongr.eq_1 : ∀ {α : Type u_6} {β : Type u_7} (e : α ≃ β),
  FreeMonoid.freeMonoidCongr e =
    { toFun := ⇑(FreeMonoid.map ⇑e), invFun := ⇑(FreeMonoid.map ⇑e.symm), left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }
-- Mathlib.Order.Compare
cmpLE.eq_1 : ∀ {α : Type u_3} [inst : LE α] [inst_1 : DecidableLE α] (x y : α),
  cmpLE x y = if x ≤ y then if y ≤ x then Ordering.eq else Ordering.lt else Ordering.gt
-- Lean.Elab.InfoTree.Types
Lean.Elab.InfoTree.brecOn_1.eq : ∀ {motive_1 : Lean.Elab.InfoTree → Sort u} {motive_2 : Lean.PersistentArray Lean.Elab.InfoTree → Sort u}
  {motive_3 : Lean.PersistentArrayNode Lean.Elab.InfoTree → Sort u} {motive_4 : Array Lean.Elab.InfoTree → Sort u}
  {motive_5 : Array (Lean.PersistentArrayNode Lean.Elab.InfoTree) → Sort u}
  {motive_6 : List Lean.Elab.InfoTree → Sort u} {motive_7 : List (Lean.PersistentArrayNode Lean.Elab.InfoTree) → Sort u}
  (t : Lean.PersistentArray Lean.Elab.InfoTree) (F_1 : (t : Lean.Elab.InfoTree) → t.below → motive_1 t)
  (F_2 : (t : Lean.PersistentArray Lean.Elab.InfoTree) → Lean.Elab.InfoTree.below_1 t → motive_2 t)
  (F_3 : (t : Lean.PersistentArrayNode Lean.Elab.InfoTree) → Lean.Elab.InfoTree.below_2 t → motive_3 t)
  (F_4 : (t : Array Lean.Elab.InfoTree) → Lean.Elab.InfoTree.below_3 t → motive_4 t)
  (F_5 : (t : Array (Lean.PersistentArrayNode Lean.Elab.InfoTree)) → Lean.Elab.InfoTree.below_4 t → motive_5 t)
  (F_6 : (t : List Lean.Elab.InfoTree) → Lean.Elab.InfoTree.below_5 t → motive_6 t)
  (F_7 : (t : List (Lean.PersistentArrayNode Lean.Elab.InfoTree)) → Lean.Elab.InfoTree.below_6 t → motive_7 t),
  Lean.Elab.InfoTree.brecOn_1 t F_1 F_2 F_3 F_4 F_5 F_6 F_7 =
    F_2 t (Lean.Elab.InfoTree.brecOn_1.go t F_1 F_2 F_3 F_4 F_5 F_6 F_7).2