mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
ContinuousLinearMap.comp_memLp' : ∀ {α : 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] {σ : 𝕜 →+* 𝕜'} [RingHomIsometric σ] (L : E →SL[σ] F) {f : α → E},
  MeasureTheory.MemLp f p μ → MeasureTheory.MemLp (⇑L ∘ f) p μ
-- Mathlib.CategoryTheory.Limits.HasLimits
/-- `hasColimitsOfSizeShrink.{v u} C` tries to obtain `HasColimitsOfSize.{v u} C`
from some other `HasColimitsOfSize C`.
 -/
CategoryTheory.Limits.hasColimitsOfSizeShrink : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasColimitsOfSize.{max v₁ v₂, max u₁ u₂, v, u} C],
  CategoryTheory.Limits.HasColimitsOfSize.{v₁, u₁, v, u} C
-- Mathlib.CategoryTheory.Functor.Basic
CategoryTheory.Functor.comp_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D)
  (G : CategoryTheory.Functor D E) {X Y : C} (f : X ⟶ Y), (F.comp G).map f = G.map (F.map f)
-- Mathlib.CategoryTheory.Subfunctor.Finite
CategoryTheory.Subfunctor.IsGeneratedBy.of_equiv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor Cᵒᵖ (Type w)}
  {G : CategoryTheory.Subfunctor F} {ι : Type w'} {X : ι → Cᵒᵖ} {x : (i : ι) → F.obj (X i)},
  G.IsGeneratedBy x → ∀ {ι' : Type w''} (e : ι' ≃ ι), G.IsGeneratedBy fun i' => x (e i')
-- Lean.Server.Rpc.RequestHandling
Lean.Server.registerRpcProcedure : Lean.Name → Lean.CoreM Unit
-- Init.Data.List.Sort.Impl
_private.Init.Data.List.Sort.Impl.0.List.mergeSort.eq_1 : ∀ {α : Type u_1} (x : α → α → Bool), [].mergeSort x = []
-- Mathlib.Data.Int.Cast.Lemmas
Int.coe_castAddHom : ∀ {α : Type u_3} [inst : AddGroupWithOne α], ⇑(Int.castAddHom α) = fun x => ↑x
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.maxKey!_eq_back!_keysArray : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.maxKey! = t.keysArray.back!
-- Std.Tactic.BVDecide.Normalize.Equal
Std.Tactic.BVDecide.Frontend.Normalize.BitVec.not_beq_not : ∀ {w : ℕ} (a b : BitVec w), (~~~a == ~~~b) = (a == b)
-- Mathlib.CategoryTheory.Triangulated.Opposite.Pretriangulated
CategoryTheory.Pretriangulated.Opposite.isomorphic_distinguished : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C],
  ∀ T₁ ∈ CategoryTheory.Pretriangulated.Opposite.distinguishedTriangles C,
    ∀ (T₂ : CategoryTheory.Pretriangulated.Triangle Cᵒᵖ) (e : T₂ ≅ T₁),
      T₂ ∈ CategoryTheory.Pretriangulated.Opposite.distinguishedTriangles C
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.bddAbove_of_small : ∀ {s : Set Ordinal.{u}} [Small.{u, u + 1} ↑s], BddAbove s
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.min?_eq_head?_toList : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp], t.WF → t.min? = t.toList.head?
-- Mathlib.MeasureTheory.Measure.Haar.NormedSpace
MeasureTheory.Measure.setIntegral_comp_smul_of_pos : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E] [BorelSpace E]
  [FiniteDimensional ℝ E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] {F : Type u_2}
  [inst_6 : NormedAddCommGroup F] [inst_7 : NormedSpace ℝ F] (f : E → F) {R : ℝ} (s : Set E),
  0 < R → ∫ (x : E) in s, f (R • x) ∂μ = (R ^ Module.finrank ℝ E)⁻¹ • ∫ (x : E) in R • s, f x ∂μ
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks
CategoryTheory.Limits.instIsIsoPushoutComparison : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} [inst_2 : CategoryTheory.Limits.HasPushout f g]
  [inst_3 : CategoryTheory.Limits.HasPushout (G.map f) (G.map g)]
  [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span f g) G],
  CategoryTheory.IsIso (CategoryTheory.Limits.pushoutComparison G f g)
-- Mathlib.Analysis.InnerProductSpace.Defs
/-- A structure requiring that a scalar product is positive definite. Some theorems that
require these assumptions are put under section `InnerProductSpace.Core`.  -/
InnerProductSpace.Core : (𝕜 : Type u_4) → (F : Type u_5) → [inst : RCLike 𝕜] → [inst_1 : AddCommGroup F] → [Module 𝕜 F] → Type (max u_4 u_5)
-- Std.Data.HashMap.Lemmas
Std.HashMap.Equiv.getElem_eq : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} (hk : k ∈ m₁) (h : m₁.Equiv m₂), m₁[k] = m₂[k]
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.instDiv.eq_1 : ∀ {α : Type u_1} {γ : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace γ]
  [inst_2 : Group γ] [inst_3 : IsTopologicalGroup γ],
  MeasureTheory.AEEqFun.instDiv = { div := MeasureTheory.AEEqFun.comp₂ Div.div ⋯ }
-- Mathlib.Tactic.NormNum.Pow
Mathlib.Meta.NormNum.isNat_zpow_neg : ∀ {α : Type u_1} [inst : DivisionSemiring α] {a : α} {b : ℤ} {nb ne : ℕ},
  Mathlib.Meta.NormNum.IsInt b (Int.negOfNat nb) →
    Mathlib.Meta.NormNum.IsNat (a ^ nb)⁻¹ ne → Mathlib.Meta.NormNum.IsNat (a ^ b) ne
-- Mathlib.Data.List.Rotate
List.mem_cyclicPermutations_self : ∀ {α : Type u} (l : List α), l ∈ l.cyclicPermutations
-- Mathlib.RingTheory.Adjoin.Singleton
/-- **Alias** of `Algebra.RingHom.adjoinAlgebraMap_surjective`. -/
Algebra.RingHom.adjoin_algebraMap_surjective : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} [inst : CommSemiring A] [inst_1 : CommSemiring B]
  [inst_2 : CommSemiring C] [inst_3 : Algebra A B] [inst_4 : Algebra B C] [inst_5 : Algebra A C]
  [inst_6 : IsScalarTower A B C] (b : B), Function.Surjective ⇑(Algebra.RingHom.adjoinAlgebraMap b)
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
/-- A zero morphism `0 : X ⟶ X` is an isomorphism if and only if
`X` is isomorphic to the zero object.
 -/
CategoryTheory.Limits.isIsoZeroSelfEquivIsoZero : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject C] → (X : C) → CategoryTheory.IsIso 0 ≃ (X ≅ 0)
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.coprodComparisonNatIso_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{w, u₂} D]
  (F : CategoryTheory.Functor C D) [inst_2 : CategoryTheory.Limits.HasBinaryCoproducts C]
  [inst_3 : CategoryTheory.Limits.HasBinaryCoproducts D] (A : C)
  [inst_4 : ∀ (B : C), CategoryTheory.IsIso (CategoryTheory.Limits.coprodComparison F A B)],
  (CategoryTheory.Limits.coprodComparisonNatIso F A).hom = CategoryTheory.Limits.coprodComparisonNatTrans F A
-- Mathlib.Order.RelIso.Basic
RelIso.self_comp_symm : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (e : r ≃r s), ⇑e ∘ ⇑e.symm = id
-- Mathlib.Data.Ordmap.Invariants
Ordnode.BalancedSz.eq_1 : ∀ (l r : ℕ), Ordnode.BalancedSz l r = (l + r ≤ 1 ∨ l ≤ Ordnode.delta * r ∧ r ≤ Ordnode.delta * l)
-- Mathlib.Algebra.MonoidAlgebra.Module
/-- The `R`-submodule of all elements of `S[M]` supported on a subset `s` of `M`.  -/
AddMonoidAlgebra.supported : (R : Type u_1) →
  (S : Type u_2) →
    {M : Type u_3} →
      [inst : Semiring R] → [inst_1 : Semiring S] → [inst_2 : Module R S] → Set M → Submodule R (AddMonoidAlgebra S M)
-- Mathlib.Algebra.Order.Hom.MonoidWithZero
OrderMonoidWithZeroHom.coe_copy : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : MulZeroOneClass α]
  [inst_3 : MulZeroOneClass β] (f : α →*₀o β) (f' : α → β) (h : f' = ⇑f), ⇑(f.copy f' h) = f'
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get?_empty : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} [Std.TransOrd α] {a : α},
  Std.DTreeMap.Internal.Impl.Const.get? Std.DTreeMap.Internal.Impl.empty a = none
-- Mathlib.Tactic.Polynomial.Basic
/-- Run the `polynomial_pre` simpset to turn nonstandard spellings of `algebraMap` such as
`Polynomial.C` into `algebraMap`  -/
Mathlib.Tactic.Polynomial.preprocess : Lean.Expr → Lean.MetaM Lean.Meta.Simp.Result
-- Mathlib.FieldTheory.Perfect
bijective_iterateFrobenius : ∀ (R : Type u_1) (p n : ℕ) [inst : CommSemiring R] [inst_1 : ExpChar R p] [PerfectRing R p],
  Function.Bijective ⇑(iterateFrobenius R p n)
-- Mathlib.Algebra.Polynomial.Degree.Lemmas
Polynomial.natDegree_mul_C_le : ∀ {R : Type u} [inst : Semiring R] (f : Polynomial R) (a : R), (f * Polynomial.C a).natDegree ≤ f.natDegree
-- Mathlib.RingTheory.Lasker
Submodule.localized₀FrameHom.congr_simp : ∀ {R : Type u_1} {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] (p p_1 : Submonoid R) (e_p : p = p_1)
  (f f_1 : M →ₗ[R] N) (e_f : f = f_1) [inst_5 : IsLocalizedModule p f],
  Submodule.localized₀FrameHom p f = Submodule.localized₀FrameHom p_1 f_1
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.getD_alter : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β}
  [inst_2 : EquivBEq α] [LawfulHashable α] {k k' : α} {fallback : β} {f : Option β → Option β},
  m.WF →
    Std.DHashMap.Raw.Const.getD (Std.DHashMap.Raw.Const.alter m k f) k' fallback =
      if (k == k') = true then (f (Std.DHashMap.Raw.Const.get? m k)).getD fallback
      else Std.DHashMap.Raw.Const.getD m k' fallback
-- Mathlib.Algebra.Polynomial.Degree.Lemmas
Polynomial.natDegree_sum_eq_of_disjoint : ∀ {R : Type u} {S : Type v} [inst : Semiring R] (f : S → Polynomial R) (s : Finset S),
  {i | i ∈ s ∧ f i ≠ 0}.Pairwise (Function.onFun Ne (Polynomial.natDegree ∘ f)) →
    (s.sum f).natDegree = s.sup fun i => (f i).natDegree
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.isSome_get?_iff_mem : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {a : α},
  (m.get? a).isSome = true ↔ a ∈ m
-- Mathlib.Order.SetNotation
/-- Indexed union of a family of sets  -/
Set.iUnion : {α : Type u} → {ι : Sort v} → (ι → Set α) → Set α
-- Mathlib.Data.Finsupp.Multiset
Multiset.toFinsupp_strictMono : ∀ {ι : Type u_3} [inst : DecidableEq ι], StrictMono ⇑Multiset.toFinsupp
-- Mathlib.Order.SupClosed
IsSublattice.inter : ∀ {α : Type u_3} [inst : Lattice α] {s t : Set α}, IsSublattice s → IsSublattice t → IsSublattice (s ∩ t)
-- Init.Data.List.ControlImpl
/-- Applies a monadic function that returns a list to each element of a list, from left to right, and
concatenates the resulting lists.
 -/
List.flatMapMTR : {m : Type u → Type v} → [Monad m] → {α : Type w} → {β : Type u} → (α → m (List β)) → List α → m (List β)
-- Mathlib.Order.Comparable
/-- **Alias** of `CompRel.of_antisymmRel_of_compRel`. -/
AntisymmRel.trans_compRel : ∀ {α : Type u_1} {a b c : α} [inst : Preorder α],
  AntisymmRel (fun x1 x2 => x1 ≤ x2) a b → CompRel (fun x1 x2 => x1 ≤ x2) b c → CompRel (fun x1 x2 => x1 ≤ x2) a c
-- Mathlib.CategoryTheory.Subfunctor.Basic
CategoryTheory.Subfunctor.mk.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C (Type w)}
  (obj obj_1 : (U : C) → Set (F.obj U)) (e_obj : obj = obj_1)
  (map : ∀ {U V : C} (i : U ⟶ V), obj U ⊆ ⇑(CategoryTheory.ConcreteCategory.hom (F.map i)) ⁻¹' obj V),
  { obj := obj, map := map } = { obj := obj_1, map := ⋯ }
-- Mathlib.Data.List.Sigma
List.nodupKeys_iff_pairwise : ∀ {α : Type u} {β : α → Type v} {l : List (Sigma β)}, l.NodupKeys ↔ List.Pairwise (fun s s' => s.fst ≠ s'.fst) l
-- Mathlib.RingTheory.HahnSeries.HahnEmbedding
hahnEmbedding_isOrderedModule_rat : ∀ (M : Type u_1) [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M] [inst_3 : Module ℚ M]
  [IsOrderedModule ℚ M],
  ∃ f,
    StrictMono ⇑f ∧ ∀ (a : M), ArchimedeanClass.mk a = (FiniteArchimedeanClass.withTopOrderIso M) (ofLex (f a)).orderTop
-- Init.Data.Array.Count
Array.boole_getElem_le_count : ∀ {α : Type u_1} [inst : BEq α] {xs : Array α} {i : ℕ} {a : α} (h : i < xs.size),
  (if (xs[i] == a) = true then 1 else 0) ≤ Array.count a xs
-- Init.Data.Nat.Basic
Nat.instTransLt : Trans (fun x1 x2 => x1 < x2) (fun x1 x2 => x1 < x2) fun x1 x2 => x1 < x2
-- Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
NNReal.agm_eq_agm_gm_am : ∀ {x y : NNReal}, x.agm y = (NNReal.sqrt (x * y)).agm ((x + y) / 2)
-- Mathlib.Algebra.Category.BoolRing
BoolRing.instInhabited : Inhabited BoolRing
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.verts_iSup : ∀ {ι : Sort u_1} {V : Type u} {G : SimpleGraph V} {f : ι → G.Subgraph}, (⨆ i, f i).verts = ⋃ i, (f i).verts
-- Mathlib.Data.ENat.Basic
/-- **Alias** of `ENat.top_ne_natCast`. -/
ENat.top_ne_coe : ∀ (a : ℕ), ⊤ ≠ ↑a
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.isUnit_iff_valued_eq_one : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] {K : Type u_2} [inst_2 : Field K]
  [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] {v : IsDedekindDomain.HeightOneSpectrum R}
  {a : ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)}, IsUnit a ↔ Valued.v ↑a = 1
-- Mathlib.Tactic.CrossRefAttribute
Mathlib.CrossRef.Database.stacks.sizeOf_spec : sizeOf Mathlib.CrossRef.Database.stacks = 1
-- Lean.Data.Lsp.Basic
Lean.Lsp.instFromJsonChangeAnnotation : Lean.FromJson Lean.Lsp.ChangeAnnotation
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.HasColimit.isoOfEquivalence.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  {C : Type u} [inst_2 : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor J C}
  [inst_3 : CategoryTheory.Limits.HasColimit F] {G : CategoryTheory.Functor K C}
  [inst_4 : CategoryTheory.Limits.HasColimit G] (e : J ≌ K) (w : e.functor.comp G ≅ F),
  CategoryTheory.Limits.HasColimit.isoOfEquivalence e w =
    (CategoryTheory.Limits.colimit.isColimit F).coconePointsIsoOfEquivalence (CategoryTheory.Limits.colimit.isColimit G)
      e w
-- Mathlib.Algebra.Group.AddChar
AddChar.mul_eq_add : ∀ {A : Type u_2} {M : Type u_3} [inst : AddMonoid A] [inst_1 : CommMonoid M] (ψ χ : AddChar A M), ψ * χ = ψ + χ
-- Lean.Parser.Term
Lean.Parser.Term.explicit.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Algebra.Group.Subgroup.MulOpposite
AddSubgroup.unop_toSubsemigroup : ∀ {G : Type u_2} [inst : AddGroup G] (H : AddSubgroup Gᵃᵒᵖ), H.unop.toAddSubsemigroup = H.unop
-- Mathlib.RingTheory.MvPowerSeries.Trunc
MvPowerSeries.truncTotal.eq_1 : ∀ {σ : Type u_1} [inst : Finite σ] {R : Type u_4} [inst_1 : CommSemiring R] (n : ℕ),
  MvPowerSeries.truncTotal n = MvPowerSeries.truncFinset R ⋯.toFinset
-- Mathlib.Algebra.Group.Even
/-- **Alias** of the forward direction of `even_iff_exists_add_self`. -/
Even.exists_add_self : ∀ {α : Type u_2} [inst : Add α] (a : α), Even a → ∃ r, a = r + r
-- Init.Control.Lawful.Basic
/-- `seq` is associative.

Changing the nesting of `seq` calls while maintaining the order of computations results in an
equivalent computation. This means that `seq` is not doing any more than sequencing.
 -/
LawfulApplicative.seq_assoc : ∀ {f : Type u → Type v} {inst : Applicative f} [self : LawfulApplicative f] {α β γ : Type u} (x : f α) (g : f (α → β))
  (h : f (β → γ)), h <*> (g <*> x) = Function.comp <$> h <*> g <*> x
-- Mathlib.Topology.Path
Path.cast_coe : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X} (γ : Path x y) {x' y' : X} (hx : x' = x) (hy : y' = y),
  ⇑(γ.cast hx hy) = ⇑γ
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.changeFunctor_inverse : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : C ≌ D) {G : CategoryTheory.Functor C D} (iso : e.functor ≅ G), (e.changeFunctor iso).inverse = e.inverse
-- Std.Data.TreeMap.Raw.Basic
/-- Internal implementation detail of the tree map  -/
Std.TreeMap.Raw.Equiv.inner : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {m₁ m₂ : Std.TreeMap.Raw α β cmp},
  m₁.Equiv m₂ → m₁.inner.Equiv m₂.inner
-- Mathlib.MeasureTheory.Integral.Lebesgue.Basic
MeasureTheory.lintegral_indicator_const₀ : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α},
  MeasureTheory.NullMeasurableSet s μ → ∀ (c : ENNReal), ∫⁻ (a : α), s.indicator (fun x => c) a ∂μ = c * μ s
-- Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic
/-- A normal epimorphism is a morphism which is the cokernel of some morphism.  -/
CategoryTheory.NormalEpi : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y : C} → [CategoryTheory.Limits.HasZeroMorphisms C] → (X ⟶ Y) → Type (max u₁ v₁)
-- Mathlib.Algebra.Category.Ring.Colimits
CommRingCat.Colimits.Prequotient.zero : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    {F : CategoryTheory.Functor J CommRingCat} → CommRingCat.Colimits.Prequotient F
-- Mathlib.Algebra.Group.Submonoid.MulOpposite
Submonoid.coe_unop : ∀ {M : Type u_2} [inst : MulOneClass M] (x : Submonoid Mᵐᵒᵖ), ↑x.unop = MulOpposite.op ⁻¹' ↑x
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
IsPrimitiveRoot.eq_neg_one_of_two_right : ∀ {R : Type u_4} [inst : CommRing R] [NoZeroDivisors R] {ζ : R}, IsPrimitiveRoot ζ 2 → ζ = -1
-- Mathlib.Topology.Semicontinuity.Defs
UpperHemicontinuousOn.mono : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → Set β} {s t : Set α},
  UpperHemicontinuousOn f s → t ⊆ s → UpperHemicontinuousOn f t
-- Std.Internal.Parsec.Basic
/-- Consumes one element if available, otherwise errors on EOF.
 -/
Std.Internal.Parsec.skip : {ι elem idx : Type} →
  [inst : DecidableEq idx] →
    [inst_1 : DecidableEq elem] → [Std.Internal.Parsec.Input ι elem idx] → Std.Internal.Parsec ι Unit
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.image_div_const_Ioc : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α] (a b c : α),
  (fun x => x / a) '' Set.Ioc b c = Set.Ioc (b / a) (c / a)
-- Mathlib.Algebra.Lie.Classical
LieAlgebra.Orthogonal.invertiblePB : (l : Type u_4) →
  (R : Type u₂) →
    [inst : DecidableEq l] →
      [inst_1 : CommRing R] → [inst_2 : Fintype l] → [Invertible 2] → Invertible (LieAlgebra.Orthogonal.PB l R)
-- Init.Data.Range.Polymorphic.IntLemmas
Int.getElem!_toArray_rco_eq_add : ∀ {m n : ℤ} {i : ℕ}, i < (n - m).toNat → (m...n).toArray[i]! = m + ↑i
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CompletionItemKind.unit : Lean.Lsp.CompletionItemKind
-- Mathlib.Topology.Separation.CompletelyRegular
Topology.IsEmbedding.t35Space : ∀ {X : Type u} [inst : TopologicalSpace X] {Y : Type v} [inst_1 : TopologicalSpace Y] [T35Space Y] {f : X → Y},
  Topology.IsEmbedding f → T35Space X
-- Lean.Meta.DiscrTree.Main
_private.Lean.Meta.DiscrTree.Main.0.Lean.Meta.DiscrTree.getMatchLoop : {α : Type} → Array Lean.Expr → Lean.Meta.DiscrTree.Trie α → Array α → Lean.MetaM (Array α)
-- Mathlib.Topology.Sheaves.Flasque
CategoryTheory.Limits.IsTerminal.from.hcongr_5 : ∀ (C C' : Type u₁),
  C = C' →
    ∀ (inst : CategoryTheory.Category.{v₁, u₁} C) (inst' : CategoryTheory.Category.{v₁, u₁} C'),
      inst ≍ inst' →
        ∀ (X : C) (X' : C'),
          X ≍ X' →
            ∀ (t : CategoryTheory.Limits.IsTerminal X) (t' : CategoryTheory.Limits.IsTerminal X'),
              t ≍ t' → ∀ (Y : C) (Y' : C'), Y ≍ Y' → t.from Y ≍ t'.from Y'
-- Mathlib.Data.List.Sym
List.sym2_map : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (xs : List α), (List.map f xs).sym2 = List.map (Sym2.map f) xs.sym2
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basic
/-- `monomialRpow` approximates the monomial function.  -/
Tactic.ComputeAsymptotics.MultiseriesExpansion.monomialRpow_approximates : ∀ {basis : Tactic.ComputeAsymptotics.Basis} {n : Fin (List.length basis)} {r : ℝ},
  Tactic.ComputeAsymptotics.WellFormedBasis basis →
    (Tactic.ComputeAsymptotics.MultiseriesExpansion.monomialRpow basis (↑n) r).Approximates
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
/-- Characterizing the forward direction of `leftUnitor` via the universal maps.  -/
CategoryTheory.MonoidalCategory.DayConvolutionUnit.leftUnitor_hom_unit_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} V]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalCategory V]
  (U : CategoryTheory.Functor C V) [inst_4 : CategoryTheory.MonoidalCategory.DayConvolutionUnit U]
  (F : CategoryTheory.Functor C V)
  [inst_5 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow
          (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) d)
        (CategoryTheory.MonoidalCategory.tensorRight v)]
  [inst_6 : CategoryTheory.MonoidalCategory.DayConvolution U F] (y : C),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonoidalCategory.DayConvolutionUnit.can
        (F.obj y))
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.MonoidalCategory.DayConvolution.unit U F).app
          (CategoryTheory.MonoidalCategoryStruct.tensorUnit C, y))
        ((CategoryTheory.MonoidalCategory.DayConvolutionUnit.leftUnitor U F).hom.app
          (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) y))) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (F.obj y)).hom
      (F.map (CategoryTheory.MonoidalCategoryStruct.leftUnitor y).inv)
-- Mathlib.Analysis.InnerProductSpace.LinearPMap
LinearPMap.adjointAux.eq_1 : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F] {T : E →ₗ.[𝕜] F}
  [inst_5 : CompleteSpace E] (hT : Dense ↑T.domain),
  LinearPMap.adjointAux hT =
    { toFun := fun y => (InnerProductSpace.toDual 𝕜 E).symm (T.adjointDomainMkCLMExtend y), map_add' := ⋯,
      map_smul' := ⋯ }
-- Mathlib.Topology.Compactness.Lindelof
IsLindelof.union : ∀ {X : Type u} [inst : TopologicalSpace X] {s t : Set X}, IsLindelof s → IsLindelof t → IsLindelof (s ∪ t)
-- Mathlib.Algebra.Group.Submonoid.Defs
ZeroMemClass.coe_zero : ∀ {A : Type u_3} {M₁ : Type u_4} [inst : SetLike A M₁] [inst_1 : Zero M₁] [hA : ZeroMemClass A M₁] (S' : A), ↑0 = 0
-- Mathlib.Data.Complex.Basic
Complex.ofReal_comp_neg : ∀ {α : Type u_1} (f : α → ℝ), Complex.ofReal ∘ (-f) = -Complex.ofReal ∘ f
-- Mathlib.Topology.Sheaves.Stalks
TopCat.Presheaf.germ_stalkSpecializes_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C] {X : TopCat}
  (F : TopCat.Presheaf C X) {U : TopologicalSpace.Opens ↑X} {y : ↑X} (hy : y ∈ U) {x : ↑X} (h : x ⤳ y) {Z : C}
  (h_1 : F.stalk x ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.germ U y hy) (CategoryTheory.CategoryStruct.comp (F.stalkSpecializes h) h_1) =
    CategoryTheory.CategoryStruct.comp (F.germ U x ⋯) h_1
-- Mathlib.CategoryTheory.MorphismProperty.LiftingProperty
CategoryTheory.MorphismProperty.rlp_ofHoms_iff_hasLiftingProperty : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (ι : Type u_1) [Nonempty ι] {A B X Y : C} (i : A ⟶ B)
  (p : X ⟶ Y), (CategoryTheory.MorphismProperty.ofHoms fun x => i).rlp p ↔ CategoryTheory.HasLiftingProperty i p