mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Trace.Defs
/-- The `traceForm` maps `x y : S` to the trace of `x * y`.
It is a symmetric bilinear form and is nondegenerate if the extension is separable.  -/
Algebra.traceForm : (R : Type u_1) →
  (S : Type u_2) → [inst : CommRing R] → [inst_1 : CommRing S] → [inst_2 : Algebra R S] → LinearMap.BilinForm R S
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
SheafOfModules.IsFinitePresentation.exists_quasicoherentData : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} {inst_1 : ∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat}
  {inst_2 : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat} (M : SheafOfModules R)
  [self : M.IsFinitePresentation], ∃ σ, σ.IsFinitePresentation
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
/-- Given a natural transformation `τ : F ⟶ G` between functors `C ⥤ D` which preserve
the homology of a short complex `S`, and a homology data for `S`,
this is the homology map data for the morphism `S.mapNatTrans τ`
obtained by evaluating `τ`.  -/
CategoryTheory.ShortComplex.HomologyMapData.natTransApp : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
          [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] →
            {S : CategoryTheory.ShortComplex C} →
              {F G : CategoryTheory.Functor C D} →
                [inst_4 : F.PreservesZeroMorphisms] →
                  [inst_5 : G.PreservesZeroMorphisms] →
                    [inst_6 : F.PreservesLeftHomologyOf S] →
                      [inst_7 : G.PreservesLeftHomologyOf S] →
                        [inst_8 : F.PreservesRightHomologyOf S] →
                          [inst_9 : G.PreservesRightHomologyOf S] →
                            (h : S.HomologyData) →
                              (τ : F ⟶ G) →
                                CategoryTheory.ShortComplex.HomologyMapData (S.mapNatTrans τ) (h.map F) (h.map G)
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
/-- For any path `p` from `x₀` to `x₁`, we have a homotopy from `p.trans (Path.refl x₁)` to `p`.  -/
Path.Homotopy.transRefl : {X : Type u_1} → [inst : TopologicalSpace X] → {x₀ x₁ : X} → (p : Path x₀ x₁) → (p.trans (Path.refl x₁)).Homotopy p
-- Mathlib.Topology.UnitInterval
unitInterval.mul_mem : ∀ {x y : ℝ}, x ∈ unitInterval → y ∈ unitInterval → x * y ∈ unitInterval
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.pairing_same : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) (i : ι),
  P.pairing i i = 2
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.degree_C_mul_of_isUnit : ∀ {R : Type u} {a : R} [inst : Semiring R], IsUnit a → ∀ (p : Polynomial R), (Polynomial.C a * p).degree = p.degree
-- Mathlib.CategoryTheory.Join.Opposites
CategoryTheory.Join.opEquiv_inverse_obj_right_op : ∀ {C : Type u₁} (D : Type u₂) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (c : C),
  (CategoryTheory.Join.opEquiv C D).inverse.obj (CategoryTheory.Join.right (Opposite.op c)) =
    Opposite.op (CategoryTheory.Join.left c)
-- Mathlib.Algebra.Field.IsField
IsField.nontrivial : ∀ {R : Type u} [inst : Semiring R], IsField R → Nontrivial R
-- Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity
GaussianInt.prime_of_nat_prime_of_mod_four_eq_three : ∀ (p : ℕ) [Fact (Nat.Prime p)], p % 4 = 3 → Prime ↑p
-- Init.Data.SInt.Lemmas
Int8.mul_one : ∀ (a : Int8), a * 1 = a
-- Mathlib.AlgebraicTopology.SimplicialSet.Splitting
/-- The canonical splitting of a simplicial set that is given
by the nondegenerate simplices.  -/
SSet.splitting : (X : SSet) → CategoryTheory.SimplicialObject.Splitting X
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality
Polynomial.Chebyshev.integral_eval_T_real_measureT_of_ne_zero : ∀ {n : ℤ}, n ≠ 0 → ∫ (x : ℝ), Polynomial.eval x (Polynomial.Chebyshev.T ℝ n) ∂Polynomial.Chebyshev.measureT = 0
-- Mathlib.ModelTheory.PartialEquiv
FirstOrder.Language.PartialEquiv.monotone_symm : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N],
  Monotone fun f => f.symm
-- Aesop.Util.UnionFind
Aesop.UnionFind.parents : {α : Type u_1} → [inst : BEq α] → [inst_1 : Hashable α] → Aesop.UnionFind α → Array USize
-- Mathlib.LinearAlgebra.Multilinear.Basic
/-- Reinterpret an `A`-multilinear map as an `R`-multilinear map, if `A` is an algebra over `R`
and their actions on all involved modules agree with the action of `R` on `A`.  -/
MultilinearMap.restrictScalars : (R : Type uR) →
  {ι : Type uι} →
    {M₁ : ι → Type v₁} →
      {M₂ : Type v₂} →
        [inst : Semiring R] →
          [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] →
            [inst_2 : AddCommMonoid M₂] →
              [inst_3 : (i : ι) → Module R (M₁ i)] →
                [inst_4 : Module R M₂] →
                  {A : Type u_1} →
                    [inst_5 : Semiring A] →
                      [inst_6 : SMul R A] →
                        [inst_7 : (i : ι) → Module A (M₁ i)] →
                          [inst_8 : Module A M₂] →
                            [∀ (i : ι), IsScalarTower R A (M₁ i)] →
                              [IsScalarTower R A M₂] → MultilinearMap A M₁ M₂ → MultilinearMap R M₁ M₂
-- Mathlib.Tactic.Linarith.Frontend
/-- Transparency mode for identifying atomic expressions in comparisons.  -/
Mathlib.Tactic.Linarith.LinarithConfig.transparency : Mathlib.Tactic.Linarith.LinarithConfig → Lean.Meta.TransparencyMode
-- Lean.Level
Lean.LevelMVarId.mk.injEq : ∀ (name name_1 : Lean.Name), ({ name := name } = { name := name_1 }) = (name = name_1)
-- Init.Data.UInt.Bitwise
USize.ofNat_xor : ∀ (a b : ℕ), USize.ofNat (a ^^^ b) = USize.ofNat a ^^^ USize.ofNat b
-- Init.Data.UInt.Lemmas
UInt8.pow_succ : ∀ (x : UInt8) (n : ℕ), x ^ (n + 1) = x ^ n * x
-- Mathlib.MeasureTheory.Measure.Lebesgue.Integral
volume_regionBetween_eq_integral' : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {f g : α → ℝ} {s : Set α}
  [MeasureTheory.SigmaFinite μ],
  MeasureTheory.IntegrableOn f s μ →
    MeasureTheory.IntegrableOn g s μ →
      MeasurableSet s →
        f ≤ᵐ[μ.restrict s] g →
          (μ.prod MeasureTheory.volume) (regionBetween f g s) = ENNReal.ofReal (∫ (y : α) in s, (g - f) y ∂μ)
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- The Hausdorff edistance is invariant under isometries.  -/
Metric.hausdorffEDist_image : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {s t : Set α} {Φ : α → β},
  Isometry Φ → Metric.hausdorffEDist (Φ '' s) (Φ '' t) = Metric.hausdorffEDist s t
-- Mathlib.CategoryTheory.Monoidal.Center
CategoryTheory.HalfBraiding.mk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {X : C} →
        (β :
            (U : C) →
              CategoryTheory.MonoidalCategoryStruct.tensorObj X U ≅
                CategoryTheory.MonoidalCategoryStruct.tensorObj U X) →
          autoParam
              (∀ (U U' : C),
                (β (CategoryTheory.MonoidalCategoryStruct.tensorObj U U')).hom =
                  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X U U').inv
                    (CategoryTheory.CategoryStruct.comp
                      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (β U).hom U')
                      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator U X U').hom
                        (CategoryTheory.CategoryStruct.comp
                          (CategoryTheory.MonoidalCategoryStruct.whiskerLeft U (β U').hom)
                          (CategoryTheory.MonoidalCategoryStruct.associator U U' X).inv))))
              CategoryTheory.HalfBraiding.monoidal._autoParam →
            autoParam
                (∀ {U U' : C} (f : U ⟶ U'),
                  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f)
                      (β U').hom =
                    CategoryTheory.CategoryStruct.comp (β U).hom
                      (CategoryTheory.MonoidalCategoryStruct.whiskerRight f X))
                CategoryTheory.HalfBraiding.naturality._autoParam →
              CategoryTheory.HalfBraiding X
-- Mathlib.RingTheory.Ideal.Operations
Ideal.finsuppTotal_apply : ∀ {ι : Type u_1} {M : Type u_2} [inst : AddCommGroup M] {R : Type u_3} [inst_1 : CommRing R] [inst_2 : Module R M]
  (I : Ideal R) {v : ι → M} (f : ι →₀ ↥I), (Ideal.finsuppTotal ι M I v) f = f.sum fun i x => ↑x • v i
-- Mathlib.CategoryTheory.Monoidal.Braided.Multifunctor
CategoryTheory.BraidedCategory.Hexagon.functor₁₃₂_obj_obj_map : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C] (G k : C)
  {X Y : C} (f : X ⟶ Y),
  (((CategoryTheory.BraidedCategory.Hexagon.functor₁₃₂ C).obj G).obj k).map f =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator G X k).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft G (CategoryTheory.MonoidalCategoryStruct.whiskerRight f k))
        (CategoryTheory.MonoidalCategoryStruct.associator G Y k).inv)
-- Std.Data.DTreeMap.Internal.Zipper
_private.Std.Data.DTreeMap.Internal.Zipper.0.Std.DTreeMap.Internal.Impl.toListModel.match_1.eq_2 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : Std.DTreeMap.Internal.Impl α β → Sort u_3) (size : ℕ) (k : α) (v : β k)
  (l r : Std.DTreeMap.Internal.Impl α β) (h_1 : Unit → motive Std.DTreeMap.Internal.Impl.leaf)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β k) → (l r : Std.DTreeMap.Internal.Impl α β) → motive (Std.DTreeMap.Internal.Impl.inner size k v l r)),
  (match Std.DTreeMap.Internal.Impl.inner size k v l r with
    | Std.DTreeMap.Internal.Impl.leaf => h_1 ()
    | Std.DTreeMap.Internal.Impl.inner size k v l r => h_2 size k v l r) =
    h_2 size k v l r
-- Mathlib.Analysis.Normed.Module.MStructure
IsLprojection.proj : ∀ {X : Type u_1} [inst : NormedAddCommGroup X] {M : Type u_2} [inst_1 : Ring M] [inst_2 : Module M X] {P : M},
  IsLprojection X P → IsIdempotentElem P
-- Mathlib.Data.List.Defs
List.Forall.eq_2 : ∀ {α : Type u_1} (p : α → Prop) (x_1 : α), List.Forall p [x_1] = p x_1
-- Mathlib.Data.Part
Part.mem_ofOption : ∀ {α : Type u_1} {a : α} {o : Option α}, a ∈ ↑o ↔ a ∈ o
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
CategoryTheory.ChosenPullbacksAlong.isoInv_pullback_map_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Y X : C} (f : Y ≅ X) {Y_1 Z : CategoryTheory.Over Y}
  (g : Y_1 ⟶ Z), ((CategoryTheory.ChosenPullbacksAlong.pullback f.inv).map g).left = CategoryTheory.Over.Hom.left g
-- Mathlib.Topology.Hom.ContinuousEvalConst
ContinuousAt.eval_const : ∀ {F : Type u_1} {α : Type u_2} {X : Type u_3} {Z : Type u_4} [inst : FunLike F α X] [inst_1 : TopologicalSpace F]
  [inst_2 : TopologicalSpace X] [ContinuousEvalConst F α X] [inst_4 : TopologicalSpace Z] {f : Z → F} {z : Z},
  ContinuousAt f z → ∀ (x : α), ContinuousAt (fun x_1 => (f x_1) x) z
-- Std.Do.Triple.SpecLemmas
/-- Specification for `repeatM`. The user supplies a (possibly state-dependent) termination
`measure`, an invariant, and a step `Triple` whose pre asserts the variant evaluates to `ma`
and the in-progress invariant holds, and whose post either continues with a strictly smaller
variant value (the invariant still holding) or finishes with the `.inr` invariant.
 -/
Std.Do.Spec.repeatM : ∀ {α β : Type u} {m : Type u → Type v} {ps : Std.Do.PostShape} [inst : Monad m] [Lean.Order.MonadTail m]
  [inst_2 : Std.Do.WPMonad m ps] {init : α} {f : α → m (α ⊕ β)} [inst_3 : Nonempty β]
  (measure : Std.Do.WhileVariant α ps) (inv : Std.Do.WhileInvariant α β ps),
  (∀ (a : α) (ma : ℕ),
      ⦃measure.eval a ma ∧ inv.1 (Sum.inl a)⦄
        f a ⦃(fun r =>
          match r with
          | Sum.inl a' => spred(∃ ma', measure.eval a' ma' ∧ ⌜ma' < ma⌝ ∧ inv.1 (Sum.inl a'))
          | Sum.inr b => inv.1 (Sum.inr b),
          inv.2)⦄) →
    ⦃inv.1 (Sum.inl init)⦄ repeatM f init ⦃(fun b => inv.1 (Sum.inr b), inv.2)⦄
-- Mathlib.Algebra.BigOperators.Finprod
/-- Given a family of sets `t : ι → Set α`, a finite set `I` in the index type such that all sets
`t i`, `i ∈ I`, are finite, if all `t i`, `i ∈ I`, are pairwise disjoint, then the product of `f a`
over `a ∈ ⋃ i ∈ I, t i` is equal to the product over `i ∈ I` of the products of `f a` over
`a ∈ t i`.  -/
finprod_mem_biUnion : ∀ {α : Type u_1} {ι : Type u_3} {M : Type u_5} [inst : CommMonoid M] {f : α → M} {I : Set ι} {t : ι → Set α},
  I.PairwiseDisjoint t →
    I.Finite →
      (∀ i ∈ I, (t i).Finite) →
        ∏ᶠ (a : α) (_ : a ∈ ⋃ x ∈ I, t x), f a = ∏ᶠ (i : ι) (_ : i ∈ I) (j : α) (_ : j ∈ t i), f j
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MultispanIndex.inj_fstSigmaMapOfIsColimit : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape}
  (I : CategoryTheory.Limits.MultispanIndex J C) {c : CategoryTheory.Limits.Cofan I.left}
  (d : CategoryTheory.Limits.Cofan I.right) (hc : CategoryTheory.Limits.IsColimit c) (i : J.L),
  CategoryTheory.CategoryStruct.comp (c.inj i) (I.fstSigmaMapOfIsColimit d hc) =
    CategoryTheory.CategoryStruct.comp (I.fst i) (d.inj (J.fst i))
-- Mathlib.Combinatorics.SimpleGraph.Copy
/-- **Alias** of `SimpleGraph.IsContained.mono_right`. -/
SimpleGraph.IsContained.trans_le : ∀ {α : Type u_4} {β : Type u_5} {A : SimpleGraph α} {B B' : SimpleGraph β}, A.IsContained B → B ≤ B' → A.IsContained B'
-- Mathlib.MeasureTheory.Integral.Bochner.L1
MeasureTheory.weightedSMul_apply : ∀ {α : Type u_1} {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] {m : MeasurableSpace α}
  (μ : MeasureTheory.Measure α) (s : Set α) (x : F), (MeasureTheory.weightedSMul μ s) x = μ.real s • x
-- Mathlib.Data.Real.Embedding
/-- Mapping `M` to `ℝ`, defined as the supremum of `ratLt' x`.  -/
Archimedean.embedRealFun : {M : Type u_1} → [AddCommGroup M] → [LinearOrder M] → [One M] → M → ℝ
-- Std.Async.System
Std.Async.System.instDecidableEqGroupId : DecidableEq Std.Async.System.GroupId
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Cat
CategoryTheory.Monoidal.leftUnitor_inv : ∀ (C : CategoryTheory.Cat),
  (CategoryTheory.MonoidalCategoryStruct.leftUnitor C).inv =
    (CategoryTheory.Prod.sectR { down := { as := PUnit.unit } } ↑C).toCatHom
-- Mathlib.LinearAlgebra.Pi
LinearMap.coe_piMap : ∀ {R : Type u} {ι : Type x} [inst : Semiring R] {φ : ι → Type i} [inst_1 : (i : ι) → AddCommMonoid (φ i)]
  [inst_2 : (i : ι) → Module R (φ i)] {ψ : ι → Type u_1} [inst_3 : (i : ι) → AddCommMonoid (ψ i)]
  [inst_4 : (i : ι) → Module R (ψ i)] (f : (i : ι) → φ i →ₗ[R] ψ i), ⇑(LinearMap.piMap f) = Pi.map fun i => ⇑(f i)
-- Mathlib.Computability.ContextFreeGrammar
/-- Add extra postfix to context-free rewriting.  -/
ContextFreeRule.Rewrites.append_right : ∀ {T : Type u_1} {N : Type u_2} {r : ContextFreeRule T N} {u v : List (Symbol T N)},
  r.Rewrites u v → ∀ (p : List (Symbol T N)), r.Rewrites (u ++ p) (v ++ p)
-- Std.Tactic.BVDecide.LRAT.Internal.Clause
Std.Tactic.BVDecide.LRAT.Internal.Clause.contains : {α : outParam (Type u)} →
  {β : Type v} → [self : Std.Tactic.BVDecide.LRAT.Internal.Clause α β] → β → Std.Sat.Literal α → Bool
-- Mathlib.Algebra.Lie.Weights.Cartan
/-- If the zero root subalgebra of a nilpotent Lie subalgebra `H` is just `H` then `H` is a Cartan
subalgebra.

When `L` is Noetherian, it follows from Engel's theorem that the converse holds. See
`LieAlgebra.zeroRootSubalgebra_eq_iff_is_cartan`  -/
LieAlgebra.is_cartan_of_zeroRootSubalgebra_eq : ∀ (R : Type u_1) (L : Type u_2) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  (H : LieSubalgebra R L) [inst_3 : LieRing.IsNilpotent ↥H],
  LieAlgebra.zeroRootSubalgebra R L H = H → H.IsCartanSubalgebra
-- Mathlib.Data.Rel
SetRel.IsRefl.sInter : ∀ {α : Type u_1} {ℛ : Set (SetRel α α)}, (∀ R ∈ ℛ, R.IsRefl) → SetRel.IsRefl (⋂₀ ℛ)
-- Mathlib.Algebra.Group.Hom.Defs
OneHom.ext : ∀ {M : Type u_4} {N : Type u_5} [inst : One M] [inst_1 : One N] ⦃f g : OneHom M N⦄, (∀ (x : M), f x = g x) → f = g
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Functor.mapConePostcomposeEquivalenceFunctor_hom_hom : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {D : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} D] (H : CategoryTheory.Functor C D)
  {F G : CategoryTheory.Functor J C} {α : F ≅ G} {c : CategoryTheory.Limits.Cone F},
  H.mapConePostcomposeEquivalenceFunctor.hom.hom = CategoryTheory.CategoryStruct.id (H.obj c.pt)
-- Init.Data.SInt.Lemmas
ISize.ofIntClamp_int16ToInt : ∀ (x : Int16), ISize.ofIntClamp x.toInt = x.toISize
-- Init.Data.Format.Basic
Std.instInhabitedFormat : Inhabited Std.Format
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.Pi.lift_π : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {β : Type w} {f : β → C}
  [inst_1 : CategoryTheory.Limits.HasProduct f] {P : C} (p : (b : β) → P ⟶ f b) (b : β),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.lift p) (CategoryTheory.Limits.Pi.π f b) = p b
-- Mathlib.Data.Finset.Lattice.Fold
Finset.sup_eq_zero : ∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {s : Finset β} {f : β → α}
  [inst_2 : Zero α] [IsBotZeroClass α], s.sup f = 0 ↔ ∀ i ∈ s, f i = 0
-- Lean.Elab.PreDefinition.TerminationHint
Lean.Elab.TerminationHints.terminationBy? : Lean.Elab.TerminationHints → Option Lean.Elab.TerminationBy
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
ContinuousLinearMap.coeFn_compLpL : ∀ {α : Type u_1} {E : Type u_4} {F : Type u_5} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F] {𝕜 : Type u_6} {𝕜' : Type u_7}
  [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜'] [inst_4 : NormedSpace 𝕜 E]
  [inst_5 : NormedSpace 𝕜' F] {σ : 𝕜 →+* 𝕜'} [inst_6 : RingHomIsometric σ] [inst_7 : Fact (1 ≤ p)] (L : E →SL[σ] F)
  (f : ↥(MeasureTheory.Lp E p μ)), ↑↑((ContinuousLinearMap.compLpL p μ L) f) =ᵐ[μ] fun a => L (↑↑f a)
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.instAdd : {α : Type u_1} →
  {β : Type u_2} →
    [inst : Field α] →
      [inst_1 : LinearOrder α] →
        [inst_2 : IsStrictOrderedRing α] →
          [inst_3 : Ring β] → {abv : β → α} → [IsAbsoluteValue abv] → Add (CauSeq β abv)
-- Mathlib.Tactic.Linter.Style
/-- The "openClassical" linter emits a warning on `open Classical` statements which are not
scoped to a single declaration. A non-scoped `open Classical` can hide that some theorem statements
would be better stated with explicit decidability statements.
 -/
_private.Mathlib.Tactic.Linter.Style.0.Mathlib.Linter.Style.openClassical.openClassicalLinter : Lean.Linter
-- Mathlib.Algebra.Category.MonCat.Basic
AddCommMonCat.uliftFunctor_map : ∀ {x x_1 : AddCommMonCat} (f : x ⟶ x_1),
  AddCommMonCat.uliftFunctor.map f =
    AddCommMonCat.ofHom
      (AddEquiv.ulift.symm.toAddMonoidHom.comp ((AddCommMonCat.Hom.hom f).comp AddEquiv.ulift.toAddMonoidHom))
-- Mathlib.Analysis.Convex.Quasiconvex
/-- If `f` is quasiconcave, then its under-levels are connected.  -/
QuasiconvexOn.isPreconnected_preimage_subtype : ∀ {E : Type u_4} [inst : AddCommGroup E] [inst_1 : Module ℝ E] [inst_2 : TopologicalSpace E] [IsTopologicalAddGroup E]
  [ContinuousSMul ℝ E] {β : Type u_5} [inst_5 : Preorder β] {f : E → β} {s : Set E} {t : β},
  QuasiconvexOn ℝ s f → IsPreconnected (Subtype.val ⁻¹' f ⁻¹' Set.Iic t)
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
Finpartition.IsUniform.mono : ∀ {α : Type u_1} {𝕜 : Type u_2} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : DecidableEq α] {A : Finset α} {P : Finpartition A} {G : SimpleGraph α} [inst_4 : DecidableRel G.Adj]
  {ε ε' : 𝕜}, P.IsUniform G ε → ε ≤ ε' → P.IsUniform G ε'
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.isEmpty_insertMany_empty_list : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} [Std.TransOrd α] {l : List (α × β)},
  (↑(Std.DTreeMap.Internal.Impl.Const.insertMany Std.DTreeMap.Internal.Impl.empty l ⋯)).isEmpty = l.isEmpty
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.InitEntry.mk.injEq : ∀ {α : Type} (key : Lean.Meta.LazyDiscrTree.Key) (entry : Lean.Meta.LazyDiscrTree.LazyEntry α)
  (key_1 : Lean.Meta.LazyDiscrTree.Key) (entry_1 : Lean.Meta.LazyDiscrTree.LazyEntry α),
  ({ key := key, entry := entry } = { key := key_1, entry := entry_1 }) = (key = key_1 ∧ entry = entry_1)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Real.cos_ne_zero_iff : ∀ {θ : ℝ}, Real.cos θ ≠ 0 ↔ ∀ (k : ℤ), θ ≠ (2 * ↑k + 1) * Real.pi / 2
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Mon.mult : Lean.Grind.CommRing.Power → Lean.Grind.CommRing.Mon → Lean.Grind.CommRing.Mon
-- Mathlib.Topology.Maps.Proper.Basic
isProperMap_iff_ultrafilter_of_t2 : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y} [T2Space Y],
  IsProperMap f ↔ Continuous f ∧ ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Filter.Tendsto f (↑𝒰) (nhds y) → ∃ x, ↑𝒰 ≤ nhds x
-- Mathlib.Data.Finset.MulAntidiagonal
/-- **Alias** of `Finset.antidiagonal`.

---

`Finset.antidiagonal hs ht a` is the set of all pairs of an element in
`s` and an element in `t` that add to `a`, but its construction requires proofs that `s` and `t` are
well-ordered.  -/
Finset.addAntidiagonal : {α : Type u_1} →
  [inst : AddCommMonoid α] →
    [inst_1 : PartialOrder α] → [IsOrderedCancelAddMonoid α] → {s t : Set α} → s.IsPWO → t.IsPWO → α → Finset (α × α)
-- Mathlib.Computability.TuringMachine.Tape
/-- The `flatMap` function on lists is well defined on `ListBlank`s provided that the default
element is sent to a sequence of default elements.  -/
Turing.ListBlank.flatMap : {Γ : Type u_1} →
  {Γ' : Type u_2} →
    [inst : Inhabited Γ] →
      [inst_1 : Inhabited Γ'] →
        Turing.ListBlank Γ → (f : Γ → List Γ') → (∃ n, f default = List.replicate n default) → Turing.ListBlank Γ'
-- Mathlib.Computability.TuringMachine.Computable
/-- A bundled TM2 (an equivalent of the classical Turing machine, defined starting from
the namespace `Turing.TM2` in `StackTuringMachine.lean`), with an input and output stack,
a main function, an initial state and some finiteness guarantees.  -/
Turing.FinTM2 : Type 1
-- Mathlib.ModelTheory.Arithmetic.Presburger.Basic
FirstOrder.presburgerFunc.zero.sizeOf_spec : sizeOf FirstOrder.presburgerFunc.zero = 1
-- Mathlib.Analysis.Calculus.FDeriv.Const
differentiableOn_natCast : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {s : Set E} [inst_7 : NatCast F] (n : ℕ), DifferentiableOn 𝕜 (↑n) s
-- Mathlib.Logic.Small.Set
small_setPi : ∀ {α : Type u1} {β : α → Type u2} (s : (a : α) → Set (β a)) [Small.{u, u1} α] [∀ (a : α), Small.{u, u2} ↑(s a)],
  Small.{u, max u1 u2} ↑(Set.univ.pi s)
-- Std.Data.DTreeMap.Internal.Balancing
/-- Rebalances a tree after at most one element was added to the left subtree. Uses balancing
information to show that some cases are impossible.
 -/
Std.DTreeMap.Internal.Impl.balanceL : {α : Type u} →
  {β : α → Type v} →
    (k : α) →
      β k →
        (l r : Std.DTreeMap.Internal.Impl α β) →
          l.Balanced →
            r.Balanced → Std.DTreeMap.Internal.Impl.BalanceLPrecond l.size r.size → Std.DTreeMap.Internal.Impl α β