mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Free.Coherence
CategoryTheory.FreeMonoidalCategory.normalizeMapAux.eq_6 : ∀ {C : Type u} (x : CategoryTheory.FreeMonoidalCategory C),
  CategoryTheory.FreeMonoidalCategory.normalizeMapAux (CategoryTheory.FreeMonoidalCategory.Hom.ρ_hom x) =
    id
      (CategoryTheory.Discrete.natTrans fun x_1 =>
        CategoryTheory.CategoryStruct.id
          ((CategoryTheory.MonoidalCategoryStruct.tensorObj x
                  (CategoryTheory.MonoidalCategoryStruct.tensorUnit
                    (CategoryTheory.FreeMonoidalCategory C))).normalizeObj'.obj
            x_1))
-- Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Real.nullSingletonClass_volume : MeasureTheory.NullSingletonClass MeasureTheory.volume
-- Mathlib.Topology.Algebra.Group.CompactOpen
ContinuousAddMonoidHom.isEmbedding_toContinuousMap : ∀ (A : Type u_2) (B : Type u_3) [inst : AddMonoid A] [inst_1 : AddMonoid B] [inst_2 : TopologicalSpace A]
  [inst_3 : TopologicalSpace B], Topology.IsEmbedding ContinuousAddMonoidHom.toContinuousMap
-- Mathlib.Order.Lattice.Nat
Nat.sSup_of_not_bddAbove : ∀ {s : Set ℕ}, ¬BddAbove s → sSup s = 0
-- Mathlib.Order.Filter.Pointwise
Filter.HasBasis.sub : ∀ {α : Type u_2} [inst : Sub α] {f g : Filter α} {ιf : Type u_7} {ιg : Type u_8} {pf : ιf → Prop} {sf : ιf → Set α}
  {pg : ιg → Prop} {sg : ιg → Set α},
  f.HasBasis pf sf → g.HasBasis pg sg → (f - g).HasBasis (fun i => pf i.1 ∧ pg i.2) fun i => sf i.1 - sg i.2
-- Lean.Server.Requests
Lean.Server.RequestContext.mk.inj : ∀ {rpcSessions : Std.TreeMap UInt64 (IO.Ref Lean.Server.FileWorker.RpcSession) compare}
  {doc : Lean.Server.FileWorker.EditableDocument} {hLog : IO.FS.Stream} {initParams : Lean.Lsp.InitializeParams}
  {cancelTk : Lean.Server.RequestCancellationToken} {serverRequestEmitter : Lean.Server.ServerRequestEmitter}
  {rpcSessions_1 : Std.TreeMap UInt64 (IO.Ref Lean.Server.FileWorker.RpcSession) compare}
  {doc_1 : Lean.Server.FileWorker.EditableDocument} {hLog_1 : IO.FS.Stream} {initParams_1 : Lean.Lsp.InitializeParams}
  {cancelTk_1 : Lean.Server.RequestCancellationToken} {serverRequestEmitter_1 : Lean.Server.ServerRequestEmitter},
  { rpcSessions := rpcSessions, doc := doc, hLog := hLog, initParams := initParams, cancelTk := cancelTk,
        serverRequestEmitter := serverRequestEmitter } =
      { rpcSessions := rpcSessions_1, doc := doc_1, hLog := hLog_1, initParams := initParams_1, cancelTk := cancelTk_1,
        serverRequestEmitter := serverRequestEmitter_1 } →
    rpcSessions = rpcSessions_1 ∧
      doc = doc_1 ∧
        hLog = hLog_1 ∧
          initParams = initParams_1 ∧ cancelTk = cancelTk_1 ∧ serverRequestEmitter = serverRequestEmitter_1
-- Mathlib.Algebra.Group.Submonoid.Support
AddSubmonoid.IsSpanning.mem_or_neg_mem : ∀ {G : Type u_1} [inst : AddGroup G] {M : AddSubmonoid G}, M.IsSpanning → ∀ (a : G), a ∈ M ∨ -a ∈ M
-- Init.Data.Float.Model.Float
Float.Model.instMax : Max Float.Model
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.instInhabitedSigmaQuotedExProd : {u : Lean.Level} →
  {α : Q(Type u)} →
    {bt : Q(«$α») → Type} →
      {sα : Q(CommSemiring «$α»)} →
        [(e : Q(«$α»)) → Inhabited (bt e)] → Inhabited ((e : Q(«$α»)) × Mathlib.Tactic.Ring.Common.ExProd bt sα e)
-- Mathlib.Algebra.Group.Subgroup.Map
Subgroup.map_isMulCommutative : ∀ {G : Type u_1} {G' : Type u_2} [inst : Group G] [inst_1 : Group G'] (H : Subgroup G) (f : G →* G')
  [IsMulCommutative ↥H], IsMulCommutative ↥(Subgroup.map f H)
-- Init.Data.Array.Basic
/-- Applies a monadic function that returns an array to each element of an array, from left to right.
The resulting arrays are appended.
 -/
Array.flatMapM : {α : Type u} → {m : Type u_1 → Type u_2} → {β : Type u_1} → [Monad m] → (α → m (Array β)) → Array α → m (Array β)
-- Mathlib.RingTheory.ZariskisMainTheorem
Algebra.quasiFiniteAt_iff_isOpen_singleton_fiber : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [Algebra.FiniteType R S] (q : PrimeSpectrum S), Algebra.QuasiFiniteAt R q.asIdeal ↔ IsOpen {⟨q, ⋯⟩}
-- Std.Http.Protocol.H1
/-- Results from a single step of the state machine.
 -/
Std.Http.Protocol.H1.StepResult : Std.Http.Protocol.H1.Direction → Type
-- Mathlib.Tactic.Linter.DocString
/-- Try to parse `docComment` as a Verso docstring, and report any parse errors.

`fileName` is the file where this docstring is defined (default: the file currently being
elaborated).

This is a copy of the first half of `versoDocStringFromString`, which also does elaboration
(but here we only report parse errors).
 -/
_private.Mathlib.Tactic.Linter.DocString.0.Mathlib.Linter.checkVersoSyntax : String →
  optParam (Option String) none →
    Lean.Elab.Command.CommandElabM (Array (String.Pos.Raw × Lean.Parser.SyntaxStack × Lean.Parser.Error))
-- Mathlib.Algebra.Ring.Action.Pointwise.Set
Set.zero_mem_smul_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : Semiring α] [inst_1 : AddCommMonoid β] [inst_2 : Module α β] [IsDomain α]
  [Module.IsTorsionFree α β] {s : Set α} {t : Set β}, 0 ∈ s • t ↔ 0 ∈ s ∧ t.Nonempty ∨ 0 ∈ t ∧ s.Nonempty
-- Mathlib.Topology.Algebra.UniformConvergence
instZeroUniformOnFun : {α : Type u_1} → {β : Type u_2} → {𝔖 : Set (Set α)} → [Zero β] → Zero (UniformOnFun α β 𝔖)
-- Mathlib.Data.Set.Lattice.Image
Set.prod_iUnion : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {s : Set α} {t : ι → Set β}, s ×ˢ ⋃ i, t i = ⋃ i, s ×ˢ t i
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
continuousOn_cfc_nnreal_setProd_nhdsSet : ∀ {A : Type u_2} [inst : NormedRing A] [inst_1 : StarRing A] [inst_2 : NormedAlgebra ℝ A]
  [inst_3 : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [ContinuousStar A] [inst_5 : PartialOrder A]
  [inst_6 : StarOrderedRing A] [inst_7 : NonnegSpectrumClass ℝ A] [T2Space A] [IsSemitopologicalRing A]
  [CompleteSpace A] {s : Set NNReal},
  ContinuousOn (fun fa => cfc ((UniformOnFun.toFun {s}) fa.1) fa.2)
    ({f | ContinuousOn ((UniformOnFun.toFun {t | IsCompact t ∧ t ⊆ s}) f) s} ×ˢ
      {a | 0 ≤ a ∧ s ∈ nhdsSet (spectrum NNReal a)})
-- Mathlib.CategoryTheory.Limits.Shapes.Terminal
CategoryTheory.Limits.instHasColimitObjFunctorConstInitial : ∀ {J : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} J] {C : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] [inst_2 : CategoryTheory.Limits.HasInitial C],
  CategoryTheory.Limits.HasColimit ((CategoryTheory.Functor.const J).obj (⊥_ C))
-- Lean.Data.RArray
_private.Lean.Data.RArray.0.Lean.RArray.size_ofFn.go : ∀ {α : Type u_1} {n : ℕ} (f : Fin n → α) (lb ub : ℕ) (h1 : lb < ub) (h2 : ub ≤ n),
  (Lean.RArray.ofFn.go✝ f lb ub h1 h2).size = ub - lb
-- Init.Data.List.Lemmas
_private.Init.Data.List.Lemmas.0.List.getLast?.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α → Sort u_2) (h_1 : Unit → motive [])
  (h_2 : (a : α) → (as : List α) → motive (a :: as)),
  (match [] with
    | [] => h_1 ()
    | a :: as => h_2 a as) =
    h_1 ()
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.aemeasurable : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  (f : MeasureTheory.SimpleFunc α β), AEMeasurable (⇑f) μ
-- Mathlib.Probability.Moments.Variance
/-- The variance of a finite sum of pairwise independent random variables is the sum of the
variances.  -/
ProbabilityTheory.IndepFun.variance_sum : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ι : Type u_3} {X : ι → Ω → ℝ} {s : Finset ι},
  (∀ i ∈ s, MeasureTheory.MemLp (X i) 2 μ) →
    ((↑s).Pairwise fun i j => ProbabilityTheory.IndepFun (X i) (X j) μ) →
      ProbabilityTheory.variance (∑ i ∈ s, X i) μ = ∑ i ∈ s, ProbabilityTheory.variance (X i) μ
-- Lean.Elab.Coinductive
Lean.Elab.Command.CoinductiveElabData.mk.sizeOf_spec : ∀ (declId : Lean.Syntax) (declName : Lean.Name) (ref : Lean.Syntax) (modifiers : Lean.Elab.Modifiers)
  (ctorSyntax : Array Lean.Syntax) (isGreatest : Bool),
  sizeOf
      { declId := declId, declName := declName, ref := ref, modifiers := modifiers, ctorSyntax := ctorSyntax,
        isGreatest := isGreatest } =
    1 + sizeOf declId + sizeOf declName + sizeOf ref + sizeOf modifiers + sizeOf ctorSyntax + sizeOf isGreatest
-- Init.Data.Nat.Fold
_private.Init.Data.Nat.Fold.0.Nat.dfoldCast_rfl : ∀ {i n : ℕ} {α : (i : ℕ) → autoParam (i ≤ n) Nat.dfoldCast._auto_1✝ → Type u_1} (h : i ≤ n) (w : i = i) (x : α i h),
  Nat.dfoldCast✝ α w x = x
-- Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated
SSet.Truncated.Quasicategory₂.fill21 : ∀ {X : SSet.Truncated 2} [self : X.Quasicategory₂]
  {x₀ x₁ x₂ : X.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Quasicategory₂._proof_1 })}
  (e₀₁ : SSet.Truncated.Edge x₀ x₁) (e₁₂ : SSet.Truncated.Edge x₁ x₂),
  Nonempty ((e₀₂ : SSet.Truncated.Edge x₀ x₂) × e₀₁.CompStruct e₁₂ e₀₂)
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.containsThenInsertIfNew!_fst_eq_containsThenInsertIfNew_fst : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (t : Std.DTreeMap.Internal.Impl α β) (htb : t.Balanced) (a : α)
  (b : β a),
  (Std.DTreeMap.Internal.Impl.containsThenInsertIfNew! a b t).1 =
    (Std.DTreeMap.Internal.Impl.containsThenInsertIfNew a b t htb).1
-- Mathlib.Order.LatticeIntervals
Set.Ici.semilatticeSup : {α : Type u_1} → [inst : SemilatticeSup α] → {a : α} → SemilatticeSup ↑(Set.Ici a)
-- Std.Time.Time.Unit.Hour
Std.Time.Hour.instSubOffset : Sub Std.Time.Hour.Offset
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.continuous_compContinuous : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β] {δ : Type u_2}
  [inst_2 : TopologicalSpace δ] (g : C(δ, α)), Continuous fun f => f.compContinuous g
-- Mathlib.Order.BooleanAlgebra.Set
/-- **Alias** of `Set.union_sdiff_cancel`. -/
Set.union_diff_cancel : ∀ {α : Type u_1} {s t : Set α}, s ⊆ t → s ∪ t \ s = t
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.Context.simp : Lean.Meta.Grind.Context → Lean.Meta.Simp.Context
-- Init.Data.Nat.Fold
_private.Init.Data.Nat.Fold.0.Nat.dfoldRev.eq_2 : ∀ (n_2 : ℕ) (α_2 : (i : ℕ) → autoParam (i ≤ n_2 + 1) Nat.dfoldRev._auto_1 → Type u)
  (f_2 : (i : ℕ) → (h : i < n_2 + 1) → α_2 (i + 1) ⋯ → α_2 i ⋯) (init_2 : α_2 (n_2 + 1) ⋯),
  n_2.succ.dfoldRev f_2 init_2 = n_2.dfoldRev (fun i h => f_2 i ⋯) (f_2 n_2 ⋯ init_2)
-- Mathlib.CategoryTheory.Action.Monoidal
Action.FunctorCategoryEquivalence.functor_ε : ∀ (V : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} V] (G : Type u_2) [inst_1 : Monoid G]
  [inst_2 : CategoryTheory.MonoidalCategory V],
  CategoryTheory.Functor.LaxMonoidal.ε Action.FunctorCategoryEquivalence.functor =
    CategoryTheory.CategoryStruct.id
      (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Functor (CategoryTheory.SingleObj G) V))
-- Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
SSet.nonDegenerate.eq_1 : ∀ (X : SSet) (n : ℕ), X.nonDegenerate n = (X.degenerate n)ᶜ
-- Mathlib.ModelTheory.Order
FirstOrder.Language.instInfiniteOfModelDloOrderOfNonempty : ∀ (M : Type w) [inst : FirstOrder.Language.order.Structure M] [M ⊨ FirstOrder.Language.order.dlo] [Nonempty M],
  Infinite M
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.Splitting.s_r : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S : CategoryTheory.ShortComplex C} (s : S.Splitting), CategoryTheory.CategoryStruct.comp s.s s.r = 0
-- Mathlib.AlgebraicTopology.ModelCategory.PathObject
HomotopicalAlgebra.Precylinder.unop_p₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : Cᵒᵖ} (P : HomotopicalAlgebra.Precylinder A),
  P.unop.p₀ = P.i₀.unop
-- Mathlib.Data.Int.Bitwise
Int.bodd_zero : Int.bodd 0 = false
-- Mathlib.GroupTheory.Coprod.Basic
Monoid.Coprod.inst.eq_1 : ∀ {M : Type u_1} {N : Type u_2} [inst : Monoid M] [inst_1 : Monoid N],
  Monoid.Coprod.inst =
    { toMul := Monoid.Coprod.instMulOneClass.toMul, mul_assoc := ⋯, toOne := Monoid.Coprod.instMulOneClass.toOne,
      one_mul := ⋯, mul_one := ⋯, npow := npowRecAuto, npow_zero := ⋯, npow_succ := ⋯ }
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
CategoryTheory.StrictlyUnitaryPseudofunctor.comp_mapId_hom : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C] {D : Type u₃}
  [inst_2 : CategoryTheory.Bicategory D] (F : CategoryTheory.StrictlyUnitaryPseudofunctor B C)
  (G : CategoryTheory.StrictlyUnitaryPseudofunctor C D) (a : B),
  ((F.comp G).mapId a).hom = CategoryTheory.CategoryStruct.comp (G.map₂ (F.mapId a).hom) (G.mapId (F.obj a)).hom
-- Mathlib.Analysis.Complex.Exponential
Real.exp_approx_start : ∀ (x a b : ℝ), |Real.exp x - Real.expNear 0 x a| ≤ |x| ^ 0 / ↑(Nat.factorial 0) * b → |Real.exp x - a| ≤ b
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.H1CoresCoinf_X₁ : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) (S : Subgroup G) [inst_2 : S.Normal],
  (groupHomology.H1CoresCoinf A S).X₁ = groupHomology.H1 (Rep.res S.subtype A)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKeyD_union : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [EquivBEq α]
  [LawfulHashable α] {k fallback : α}, (m₁ ∪ m₂).getKeyD k fallback = m₂.getKeyD k (m₁.getKeyD k fallback)
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.contains_of_mem_toArray : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α],
  m.WF → ∀ {k : α}, k ∈ m.toArray → m.contains k = true
-- Mathlib.Algebra.Ring.Ext
NonUnitalRing.ext : ∀ {R : Type u} ⦃inst₁ inst₂ : NonUnitalRing R⦄, HAdd.hAdd = HAdd.hAdd → HMul.hMul = HMul.hMul → inst₁ = inst₂
-- Mathlib.Data.ENNReal.Basic
/-- `toReal x` returns `x` if it is real, `0` otherwise.  -/
ENNReal.toReal : ENNReal → ℝ
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
CategoryTheory.Functor.IsDenseSubsite.mapPreimage.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {J : CategoryTheory.GrothendieckTopology C}
  (K : CategoryTheory.GrothendieckTopology D) (G : CategoryTheory.Functor C D) {A : Type u_4}
  [inst_2 : CategoryTheory.Category.{v_4, u_4} A] [inst_3 : CategoryTheory.Functor.IsDenseSubsite J K G]
  (F : CategoryTheory.Sheaf J A) {X Y : C} (f : G.obj X ⟶ G.obj Y),
  CategoryTheory.Functor.IsDenseSubsite.mapPreimage K G F f =
    ⋯.amalgamate ⟨G.imageSieve f, ⋯⟩
      (fun x =>
        match x with
        | { Y := W₀, f := a, hf := ha } => F.obj.map (Exists.choose ha).op)
      ⋯
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey!_eq_get!_getKey? : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.WF → ∀ {a : α}, t.getKey! a = (t.getKey? a).get!
-- Mathlib.Analysis.Complex.Convex
/-- A version of `convexHull_prod` for `Set.reProdIm`.  -/
Complex.convexHull_reProdIm : ∀ (s t : Set ℝ), (convexHull ℝ) (s ×ℂ t) = (convexHull ℝ) s ×ℂ (convexHull ℝ) t
-- Mathlib.Data.Prod.Lex
/-- Variant of `Prod.Lex.toLex_le_toLex` for partial orders.  -/
Prod.Lex.toLex_le_toLex' : ∀ {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst_1 : Preorder β] {x y : α × β},
  toLex x ≤ toLex y ↔ x.1 ≤ y.1 ∧ (x.1 = y.1 → x.2 ≤ y.2)
-- Mathlib.MeasureTheory.Measure.AEMeasurable
aemeasurable_indicator_iff₀ : ∀ {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [inst : MeasurableSpace β] {f : α → β}
  {μ : MeasureTheory.Measure α} [inst_1 : Zero β] {s : Set α},
  MeasureTheory.NullMeasurableSet s μ → (AEMeasurable (s.indicator f) μ ↔ AEMeasurable f (μ.restrict s))
-- Mathlib.Data.List.Sigma
List.dlookup.congr_simp : ∀ {α : Type u} {β : α → Type v} {inst : DecidableEq α} [inst_1 : DecidableEq α] (a : α) (a_1 a_2 : List (Sigma β)),
  a_1 = a_2 → List.dlookup a a_1 = List.dlookup a a_2
-- Mathlib.CategoryTheory.GradedObject.Unitor
CategoryTheory.GradedObject.TriangleIndexData.hp₂₃ : ∀ {I₁ : Type u_1} {I₂ : Type u_2} {I₃ : Type u_3} {J : Type u_4} [inst : Zero I₂] {r : I₁ × I₂ × I₃ → J}
  {π : I₁ × I₃ → J} (self : CategoryTheory.GradedObject.TriangleIndexData r π) (i : I₁ × I₂ × I₃),
  π (i.1, self.p₂₃ i.2) = r i
-- Mathlib.RingTheory.PowerSeries.Substitution
PowerSeries.subst_zero_eq_C_constantCoeff : ∀ {R : Type u_2} [inst : CommRing R] {τ : Type u_3} {S : Type u_4} [inst_1 : CommRing S] [inst_2 : Algebra R S]
  {f : PowerSeries R},
  PowerSeries.subst 0 f = (MvPowerSeries.map (algebraMap R S)) (MvPowerSeries.C (PowerSeries.constantCoeff f))
-- Mathlib.MeasureTheory.Function.LpSpace.ContinuousFunctions
/-- The `Lp`-norm of a bounded continuous function is at most a constant (depending on the measure
of the whole space) times its sup-norm.  -/
BoundedContinuousFunction.Lp_nnnorm_le : ∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : TopologicalSpace α] [inst_1 : BorelSpace α] [inst_2 : NormedAddCommGroup E]
  [inst_3 : SecondCountableTopologyEither α E] [inst_4 : MeasureTheory.IsFiniteMeasure μ]
  (f : BoundedContinuousFunction α E),
  ‖⟨ContinuousMap.toAEEqFun μ f.toContinuousMap, ⋯⟩‖₊ ≤ MeasureTheory.measureUnivNNReal μ ^ p.toReal⁻¹ * ‖f‖₊
-- Mathlib.Analysis.SpecialFunctions.Integrals.Basic
integral_sin_sq : ∀ {a b : ℝ}, ∫ (x : ℝ) in a..b, Real.sin x ^ 2 = (Real.sin a * Real.cos a - Real.sin b * Real.cos b + b - a) / 2
-- Mathlib.LinearAlgebra.Quotient.Basic
Submodule.liftQ_apply : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (p : Submodule R M)
  {R₂ : Type u_3} {M₂ : Type u_4} [inst_3 : Ring R₂] [inst_4 : AddCommGroup M₂] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  (f : M →ₛₗ[τ₁₂] M₂) {h : p ≤ f.ker} (x : M), (p.liftQ f h) (Submodule.Quotient.mk x) = f x
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
_private.Mathlib.Tactic.CategoryTheory.Coherence.Normalize.0.Mathlib.Tactic.BicategoryLike.evalWhiskerLeft.match_1.eq_3 : ∀ (motive : Mathlib.Tactic.BicategoryLike.Mor₁ → Mathlib.Tactic.BicategoryLike.NormalExpr → Sort u_1) (e : Lean.Expr)
  (f g : Mathlib.Tactic.BicategoryLike.Mor₁) (η : Mathlib.Tactic.BicategoryLike.NormalExpr)
  (h_1 :
    (f : Mathlib.Tactic.BicategoryLike.Mor₁) →
      (e : Mathlib.Tactic.BicategoryLike.Mor₂) →
        (α : Mathlib.Tactic.BicategoryLike.Structural) → motive f (Mathlib.Tactic.BicategoryLike.NormalExpr.nil e α))
  (h_2 :
    (f : Mathlib.Tactic.BicategoryLike.Atom₁) →
      (e : Mathlib.Tactic.BicategoryLike.Mor₂) →
        (α : Mathlib.Tactic.BicategoryLike.Structural) →
          (η : Mathlib.Tactic.BicategoryLike.WhiskerLeft) →
            (ηs : Mathlib.Tactic.BicategoryLike.NormalExpr) →
              motive (Mathlib.Tactic.BicategoryLike.Mor₁.of f) (Mathlib.Tactic.BicategoryLike.NormalExpr.cons e α η ηs))
  (h_3 :
    (e : Lean.Expr) →
      (f g : Mathlib.Tactic.BicategoryLike.Mor₁) →
        (η : Mathlib.Tactic.BicategoryLike.NormalExpr) → motive (Mathlib.Tactic.BicategoryLike.Mor₁.comp e f g) η)
  (h_4 :
    (e : Lean.Expr) →
      (a : Mathlib.Tactic.BicategoryLike.Obj) →
        (η : Mathlib.Tactic.BicategoryLike.NormalExpr) → motive (Mathlib.Tactic.BicategoryLike.Mor₁.id e a) η),
  (∀ (e : Mathlib.Tactic.BicategoryLike.Mor₂) (α : Mathlib.Tactic.BicategoryLike.Structural),
      η = Mathlib.Tactic.BicategoryLike.NormalExpr.nil e α → False) →
    (match Mathlib.Tactic.BicategoryLike.Mor₁.comp e f g, η with
      | f, Mathlib.Tactic.BicategoryLike.NormalExpr.nil e α => h_1 f e α
      | Mathlib.Tactic.BicategoryLike.Mor₁.of f, Mathlib.Tactic.BicategoryLike.NormalExpr.cons e α η ηs =>
        h_2 f e α η ηs
      | Mathlib.Tactic.BicategoryLike.Mor₁.comp e f g, η => h_3 e f g η
      | Mathlib.Tactic.BicategoryLike.Mor₁.id e a, η => h_4 e a η) =
      h_3 e f g η
-- Mathlib.Analysis.Normed.Ring.WithAbs
WithAbs.instIsScalarTower : ∀ {S : Type u_2} [inst : Semiring S] [inst_1 : PartialOrder S] {R : Type u_3} {T : Type u_4} [inst_2 : Semiring R]
  (v : AbsoluteValue R S) {P : Type u_5} [inst_3 : SMul T P] [inst_4 : SMul R T] [inst_5 : SMul R P]
  [IsScalarTower R T P], IsScalarTower (WithAbs v) T P
-- Init.Data.BitVec.Bitblast
BitVec.carry.eq_1 : ∀ {w : ℕ} (i : ℕ) (x y : BitVec w) (c : Bool),
  BitVec.carry i x y c = decide (x.toNat % 2 ^ i + y.toNat % 2 ^ i + c.toNat ≥ 2 ^ i)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
CategoryTheory.IsPullback.of_horiz_isIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P X Y Z : C} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z}
  {g : Y ⟶ Z} [CategoryTheory.IsIso fst] [CategoryTheory.IsIso g],
  CategoryTheory.CommSq fst snd f g → CategoryTheory.IsPullback fst snd f g
-- Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
CategoryTheory.Abelian.SpectralObject.SpectralSequence.homologyData_left_i : ∀ {C : Type u_1} {ι : Type u_2} {κ : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Abelian C] [inst_2 : Preorder ι] (X : CategoryTheory.Abelian.SpectralObject C ι)
  {c : ℤ → ComplexShape κ} {r₀ : ℤ} (data : CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀)
  (r r' : ℤ) (hrr' : r + 1 = r') (hr : r₀ ≤ r) (pq pq' pq'' : κ) (hpq : (c r).prev pq' = pq)
  (hpq' : (c r).next pq' = pq'') (i₀' i₀ i₁ i₂ i₃ i₃' : ι) (hi₀' : i₀' = data.i₀ r' pq' ⋯) (hi₀ : i₀ = data.i₀ r pq' ⋯)
  (hi₁ : i₁ = data.i₁ pq') (hi₂ : i₂ = data.i₂ pq') (hi₃ : i₃ = data.i₃ r pq' ⋯) (hi₃' : i₃' = data.i₃ r' pq' ⋯)
  (n₀ n₁ n₂ : ℤ) (hn₁' : n₁ = data.deg pq') [inst_3 : X.HasSpectralSequence data]
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.SpectralSequence.homologyData._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.SpectralSequence.homologyData._auto_3),
  (CategoryTheory.Abelian.SpectralObject.SpectralSequence.homologyData X data r r' hrr' hr pq pq' pq'' hpq hpq' i₀' i₀
          i₁ i₂ i₃ i₃' hi₀' hi₀ hi₁ hi₂ hi₃ hi₃' n₀ n₁ n₂ hn₁' hn₁ hn₂).left.i =
    CategoryTheory.CategoryStruct.comp (X.mapFourδ₁Toδ₀' i₀' i₀ i₁ i₂ i₃ ⋯ ⋯ ⋯ ⋯ n₀ n₁ n₂ ⋯ ⋯)
      (CategoryTheory.Abelian.SpectralObject.SpectralSequence.pageXIso X data r hr pq' i₀ i₁ i₂ i₃ hi₀ hi₁ hi₂ hi₃ n₀ n₁
          n₂ hn₁' ⋯ ⋯).inv
-- Mathlib.Logic.Equiv.Defs
Equiv.Perm.ext_iff : ∀ {α : Sort u} {σ τ : Equiv.Perm α}, σ = τ ↔ ∀ (x : α), σ x = τ x
-- Lean.Util.LeanOptions
Lean.instToJsonLeanOptions : Lean.ToJson Lean.LeanOptions
-- Mathlib.Algebra.Module.Presentation.Basic
/-- the index type for relations  -/
Module.Relations.R : {A : Type u} → [inst : Ring A] → Module.Relations A → Type w₁
-- Mathlib.Combinatorics.SimpleGraph.Bipartite
/-- `G.between s t` is bipartite if the sets `s` and `t` are disjoint.  -/
SimpleGraph.between_isBipartiteWith : ∀ {V : Type u_1} {G : SimpleGraph V} {s t : Set V}, Disjoint s t → (SimpleGraph.between s t G).IsBipartiteWith s t
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
/-- A monad equipped with the ability to construct `Atom₁` terms.  -/
Mathlib.Tactic.BicategoryLike.MkAtom₁ : (Type → Type) → Type
-- Mathlib.Order.BooleanAlgebra.Basic
inf_sdiff : ∀ {α : Type u} {x y z : α} [inst : GeneralizedBooleanAlgebra α], (x ⊓ y) \ z = x \ z ⊓ y \ z