mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Normed.Unbundled.SpectralNorm
/-- If `K` is a field complete with respect to a nontrivial nonarchimedean multiplicative norm and
`L/K` is an algebraic extension, then any power-multiplicative `K`-algebra norm on `L` coincides
with the spectral norm.  -/
spectralNorm_unique : ∀ {K : Type u} [inst : NontriviallyNormedField K] {L : Type v} [inst_1 : Field L] [inst_2 : Algebra K L]
  [inst_3 : Algebra.IsAlgebraic K L] [hu : IsUltrametricDist K] [CompleteSpace K] {f : AlgebraNorm K L},
  IsPowMul ⇑f → f = spectralAlgNorm K L
-- Mathlib.Analysis.Asymptotics.Theta
/-- **Alias** of the forward direction of `Asymptotics.isTheta_const_mul_right`. -/
Asymptotics.IsTheta.of_const_mul_right : ∀ {α : Type u_1} {E : Type u_3} {𝕜 : Type u_14} [inst : Norm E] [inst_1 : NormedField 𝕜] {f : α → E} {l : Filter α}
  {c : 𝕜} {g : α → 𝕜}, c ≠ 0 → (f =Θ[l] fun x => c * g x) → f =Θ[l] g
-- Batteries.Recycling.RBTree.WF
_private.Batteries.Recycling.RBTree.WF.0.RBTree.RBNode.append.match_1.eq_4 : ∀ {α : Type u_1} (motive : RBTree.RBNode α → RBTree.RBNode α → Sort u_2) (a : RBTree.RBNode α) (x : α)
  (b c : RBTree.RBNode α) (y : α) (d : RBTree.RBNode α) (h_1 : (x : RBTree.RBNode α) → motive RBTree.RBNode.nil x)
  (h_2 : (x : RBTree.RBNode α) → motive x RBTree.RBNode.nil)
  (h_3 :
    (a : RBTree.RBNode α) →
      (x : α) →
        (b c : RBTree.RBNode α) →
          (y : α) →
            (d : RBTree.RBNode α) →
              motive (RBTree.RBNode.node RBTree.RBColor.red a x b) (RBTree.RBNode.node RBTree.RBColor.red c y d))
  (h_4 :
    (a : RBTree.RBNode α) →
      (x : α) →
        (b c : RBTree.RBNode α) →
          (y : α) →
            (d : RBTree.RBNode α) →
              motive (RBTree.RBNode.node RBTree.RBColor.black a x b) (RBTree.RBNode.node RBTree.RBColor.black c y d))
  (h_5 :
    (a l : RBTree.RBNode α) →
      (v : α) →
        (r : RBTree.RBNode α) →
          a = RBTree.RBNode.node RBTree.RBColor.black l v r →
            (b : RBTree.RBNode α) →
              (x : α) →
                (c : RBTree.RBNode α) →
                  motive (RBTree.RBNode.node RBTree.RBColor.black l v r) (RBTree.RBNode.node RBTree.RBColor.red b x c))
  (h_6 :
    (a : RBTree.RBNode α) →
      (x : α) →
        (b c l : RBTree.RBNode α) →
          (v : α) →
            (r : RBTree.RBNode α) →
              c = RBTree.RBNode.node RBTree.RBColor.black l v r →
                motive (RBTree.RBNode.node RBTree.RBColor.red a x b) (RBTree.RBNode.node RBTree.RBColor.black l v r)),
  (match RBTree.RBNode.node RBTree.RBColor.black a x b, RBTree.RBNode.node RBTree.RBColor.black c y d with
    | RBTree.RBNode.nil, x => h_1 x
    | x, RBTree.RBNode.nil => h_2 x
    | RBTree.RBNode.node RBTree.RBColor.red a x b, RBTree.RBNode.node RBTree.RBColor.red c y d => h_3 a x b c y d
    | RBTree.RBNode.node RBTree.RBColor.black a x b, RBTree.RBNode.node RBTree.RBColor.black c y d => h_4 a x b c y d
    | a@h:(RBTree.RBNode.node RBTree.RBColor.black l v r), RBTree.RBNode.node RBTree.RBColor.red b x c =>
      h_5 a l v r h b x c
    | RBTree.RBNode.node RBTree.RBColor.red a x b, c@h:(RBTree.RBNode.node RBTree.RBColor.black l v r) =>
      h_6 a x b c l v r h) =
    h_4 a x b c y d
-- Mathlib.Algebra.BigOperators.Expect
Fintype.expect_mul_expect : ∀ {ι : Type u_1} {κ : Type u_2} {M : Type u_4} [inst : Fintype ι] [inst_1 : Fintype κ] [inst_2 : Semiring M]
  [inst_3 : Module ℚ≥0 M] [IsScalarTower ℚ≥0 M M] [SMulCommClass ℚ≥0 M M] (f : ι → M) (g : κ → M),
  ((Finset.univ.expect fun i => f i) * Finset.univ.expect fun j => g j) =
    Finset.univ.expect fun i => Finset.univ.expect fun j => f i * g j
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.instNegHom : {k : Type u} → {G : Type v} → [inst : Semiring k] → [inst_1 : Monoid G] → {A B : Rep.{w, u, v} k G} → Neg (A ⟶ B)
-- Mathlib.CategoryTheory.Localization.Monoidal.Basic
CategoryTheory.Localization.Monoidal.whiskerRight_id : ∀ {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] (L : CategoryTheory.Functor C D)
  (W : CategoryTheory.MorphismProperty C) [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : W.IsMonoidal]
  [inst_4 : L.IsLocalization W] {unit : D} (ε : L.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ≅ unit)
  (X Y : CategoryTheory.LocalizedMonoidal L W ε),
  CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.CategoryStruct.id X) Y =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.maxKeyD_alter_eq_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α}
  {f : Option β → Option β},
  (t.alter k f).isEmpty = false →
    ∀ {fallback : α}, (t.alter k f).maxKeyD fallback = k ↔ (f t[k]?).isSome = true ∧ ∀ k' ∈ t, (cmp k' k).isLE = true
-- Mathlib.Analysis.Calculus.LocalExtr.Rolle
/-- **Rolle's Theorem** `deriv` version  -/
exists_deriv_eq_zero : ∀ {f : ℝ → ℝ} {a b : ℝ}, a < b → ContinuousOn f (Set.Icc a b) → f a = f b → ∃ c ∈ Set.Ioo a b, deriv f c = 0
-- Lean.Data.PersistentHashMap
Lean.PersistentHashMap.map : {α : Type u} →
  {β : Type v} →
    {σ : Type u} → {x : BEq α} → {x_1 : Hashable α} → Lean.PersistentHashMap α β → (β → σ) → Lean.PersistentHashMap α σ
-- Mathlib.Topology.EMetricSpace.Weak
instEDistWithTop : {α : Type u} → [EDist α] → EDist (WithTop α)
-- Mathlib.Tactic.ClickSuggestions.TryPremises
_private.Mathlib.Tactic.ClickSuggestions.TryPremises.0.Mathlib.Tactic.ClickSuggestions.Candidates.rw.injEq : ∀ (i : Mathlib.Tactic.ClickSuggestions.RwInfo) (arr : Array Mathlib.Tactic.ClickSuggestions.RwLemma)
  (i_1 : Mathlib.Tactic.ClickSuggestions.RwInfo) (arr_1 : Array Mathlib.Tactic.ClickSuggestions.RwLemma),
  (Mathlib.Tactic.ClickSuggestions.Candidates.rw✝ i arr = Mathlib.Tactic.ClickSuggestions.Candidates.rw✝ i_1 arr_1) =
    (i = i_1 ∧ arr = arr_1)
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddResult
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.restoreAssignments.eq_1 : ∀ {n : ℕ} (assignments : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment)
  (derivedLits : List (Std.Tactic.BVDecide.LRAT.Internal.PosFin n × Bool)),
  Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.restoreAssignments assignments derivedLits =
    List.foldl Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.clearUnit assignments derivedLits
-- Mathlib.RingTheory.Coalgebra.Convolution
/-- Non-unital and non-associative convolution ring structure on linear maps from a
coalgebra to a non-unital and non-associative algebra.  -/
LinearMap.convNonUnitalNonAssocRing : {R : Type u_1} →
  {A : Type u_3} →
    {C : Type u_5} →
      [inst : CommSemiring R] →
        [inst_1 : NonUnitalNonAssocRing A] →
          [inst_2 : Module R A] →
            [SMulCommClass R A A] →
              [IsScalarTower R A A] →
                [inst_5 : AddCommMonoid C] →
                  [inst_6 : Module R C] → [CoalgebraStruct R C] → NonUnitalNonAssocRing (WithConv (C →ₗ[R] A))
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.getD_insertMany_list_of_mem : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α],
  m.WF → ∀ {l : List α} {k fallback : α}, k ∈ m → (m.insertMany l).getD k fallback = m.getD k fallback
-- Mathlib.Topology.Maps.Basic
IsOpenMap.of_nhds_le : ∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  (∀ (x : X), nhds (f x) ≤ Filter.map f (nhds x)) → IsOpenMap f
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.Equiv.of_keys_unit_perm : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α Unit cmp}, t₁.keys.Perm t₂.keys → t₁.Equiv t₂
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Mon.concat : Lean.Grind.CommRing.Mon → Lean.Grind.CommRing.Mon → Lean.Grind.CommRing.Mon
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.toRingHom_liftAlgHom : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  [inst_3 : Algebra S R] [inst_4 : Algebra S T] (p : Polynomial R) (i : R →ₐ[S] T) (x : T)
  (h : Polynomial.eval₂ (↑i) x p = 0), ↑(AdjoinRoot.liftAlgHom p i x h) = AdjoinRoot.lift i.toRingHom x h
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafMap_π_assoc : ∀ {C₀ : Type u₀} {C : Type u} [inst : CategoryTheory.Category.{v₀, u₀} C₀] [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor C₀ C} {J₀ : CategoryTheory.GrothendieckTopology C₀}
  {J : CategoryTheory.GrothendieckTopology C} {A : Type u'} [inst_2 : CategoryTheory.Category.{v', u'} A]
  [inst_3 : CategoryTheory.Functor.IsDenseSubsite J₀ J F] (data : (X : C) → F.OneHypercoverDenseData J₀ J X)
  [inst_4 : CategoryTheory.Limits.HasLimitsOfSize.{w, w, v', u'} A] (G₀ : CategoryTheory.Sheaf J₀ A) {X Y : C}
  (f : X ⟶ Y) (i : (data X).I₀) {Z : A} (h : G₀.obj.obj (Opposite.op ((data X).X i)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafMap data G₀ f)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObjπ data G₀ X i) h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Functor.OneHypercoverDenseData.essSurj.restriction data G₀
        (CategoryTheory.CategoryStruct.comp ((data X).f i) f))
      h
-- Lean.DocString.Extension
Lean.VersoDocString.mk.sizeOf_spec : ∀ (text : Array (Lean.Doc.Block Lean.ElabInline Lean.ElabBlock))
  (subsections : Array (Lean.Doc.Part Lean.ElabInline Lean.ElabBlock Empty)),
  sizeOf { text := text, subsections := subsections } = 1 + sizeOf text + sizeOf subsections
-- Init.Data.List.Nat.Range
List.nodup_range' : ∀ {s n : ℕ} (step : optParam ℕ 1), autoParam (0 < step) List.nodup_range'._auto_1 → (List.range' s n step).Nodup
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.getD_eq : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ t₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α],
  t₁.WF → t₂.WF → t₁.Equiv t₂ → ∀ {k : α} {fallback : β k}, t₁.getD k fallback = t₂.getD k fallback
-- Mathlib.CategoryTheory.Subobject.Limits
CategoryTheory.Limits.imageSubobjectCompIso_hom_arrow : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} [inst_1 : CategoryTheory.Limits.HasEqualizers C]
  (f : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasImage f] {Y' : C} (h : Y ⟶ Y') [inst_3 : CategoryTheory.IsIso h],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobjectCompIso f h).hom
      (CategoryTheory.Limits.imageSubobject f).arrow =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.imageSubobject (CategoryTheory.CategoryStruct.comp f h)).arrow (CategoryTheory.inv h)
-- Mathlib.MeasureTheory.MeasurableSpace.Basic
/-- **Alias** of the forward direction of `measurable_iff_comap_le`. -/
Measurable.comap_le : ∀ {α : Type u_1} {β : Type u_2} {m₁ : MeasurableSpace α} {m₂ : MeasurableSpace β} {f : α → β},
  Measurable f → MeasurableSpace.comap f m₂ ≤ m₁
-- Mathlib.NumberTheory.Padics.MahlerBasis
PadicInt.instIsAddTorsionFree : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)], IsAddTorsionFree ℤ_[p]
-- Mathlib.Topology.Compactness.Paracompact
_private.Mathlib.Topology.Compactness.Paracompact.0.Option.elim'.match_1.eq_2 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (h_1 : (a : α) → motive (some a)) (h_2 : Unit → motive none),
  (match none with
    | some a => h_1 a
    | none => h_2 ()) =
    h_2 ()
-- Init.Data.Option.Lemmas
Option.getD_inj : ∀ {α : Type u_1} {o₁ o₂ : Option α},
  o₁.isSome = true → o₂.isSome = true → ∀ {fallback : α}, o₁.getD fallback = o₂.getD fallback ↔ o₁ = o₂
-- Lean.Elab.Calc
/-- Decompose `e` into `(r, a, b)`.

Remark: it assumes the last two arguments are explicit.
 -/
Lean.Elab.Term.getCalcRelation? : Lean.Expr → Lean.MetaM (Option (Lean.Expr × Lean.Expr × Lean.Expr))
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometry.preimage_ball : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} [inst_2 : SeminormedAddCommGroup E] [inst_3 : SeminormedAddCommGroup E₂] [inst_4 : Module R E]
  [inst_5 : Module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂) (x : E) (r : ℝ), ⇑f ⁻¹' Metric.ball (f x) r = Metric.ball x r
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.MapBijective
CategoryTheory.Functor.mapExt_bijective_of_preservesProjectiveObjects : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {D : Type u'}
  [inst_2 : CategoryTheory.Category.{v', u'} D] [inst_3 : CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D)
  [inst_4 : F.Additive] [inst_5 : CategoryTheory.Limits.PreservesFiniteLimits F]
  [inst_6 : CategoryTheory.Limits.PreservesFiniteColimits F] [F.Full] [F.Faithful] [inst_9 : CategoryTheory.HasExt C]
  [inst_10 : CategoryTheory.HasExt D] [CategoryTheory.EnoughProjectives C] [F.PreservesProjectiveObjects] (X Y : C)
  (n : ℕ), Function.Bijective ⇑(F.mapExtAddHom X Y n)
-- Std.Time.Zoned.Database.PosixTz
_private.Std.Time.Zoned.Database.PosixTz.0.Std.Time.TimeZone.parseBoundedNat : {lo hi : ℤ} →
  String → (optParam (ℤ → Bool) fun x => true) → Std.Internal.Parsec.String.Parser (Std.Time.Internal.Bounded.LE lo hi)
-- Mathlib.CategoryTheory.Sites.Subcanonical
CategoryTheory.GrothendieckTopology.yonedaEquiv.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C)
  [inst_1 : J.Subcanonical] {X : C} {F : CategoryTheory.Sheaf J (Type v)},
  J.yonedaEquiv = (CategoryTheory.fullyFaithfulSheafToPresheaf J (Type v)).homEquiv.trans CategoryTheory.yonedaEquiv
-- Mathlib.Algebra.Order.Hom.Monoid
OrderAddMonoidIso.symm_comp_self : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Add α] [inst_3 : Add β]
  (e : α ≃+o β), ⇑e.symm ∘ ⇑e = id
-- Mathlib.Analysis.Normed.Algebra.UnitizationL1
WithLp.unitization_norm_def : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NormedField 𝕜] [inst_1 : NonUnitalNormedRing A] [inst_2 : NormedSpace 𝕜 A]
  (x : WithLp 1 (Unitization 𝕜 A)), ‖x‖ = ‖x.ofLp.toProd.1‖ + ‖x.ofLp.toProd.2‖
-- Mathlib.MeasureTheory.Measure.Portmanteau
/-- One implication of the portmanteau theorem:
Assuming that for all Borel sets E whose boundary ∂E carries no probability mass under a
candidate limit probability measure μ we have convergence of the measures μsᵢ(E) to μ(E),
then for all open sets G we have the limsup condition μ(G) ≤ liminf μsᵢ(G).  -/
MeasureTheory.le_liminf_measure_open_of_forall_tendsto_measure : ∀ {Ω : Type u_1} {ι : Type u_2} {L : Filter ι} [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω]
  [TopologicalSpace.PseudoMetrizableSpace Ω] [OpensMeasurableSpace Ω] {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ] {μs : ι → MeasureTheory.Measure Ω}
  [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μs i)],
  (∀ {E : Set Ω}, MeasurableSet E → μ (frontier E) = 0 → Filter.Tendsto (fun i => (μs i) E) L (nhds (μ E))) →
    ∀ (G : Set Ω), IsOpen G → μ G ≤ Filter.liminf (fun i => (μs i) G) L
-- Mathlib.Algebra.Group.Subgroup.Map
MulEquiv.comapSubgroup_apply : ∀ {G : Type u_1} [inst : Group G] {H : Type u_5} [inst_1 : Group H] (f : G ≃* H) (H_1 : Subgroup H),
  f.comapSubgroup H_1 = Subgroup.comap (↑f) H_1
-- Mathlib.CategoryTheory.Join.Basic
CategoryTheory.Join.mkNatTrans.congr_simp : ∀ {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 F' : CategoryTheory.Functor (CategoryTheory.Join C D) E}
  (αₗ αₗ_1 : (CategoryTheory.Join.inclLeft C D).comp F ⟶ (CategoryTheory.Join.inclLeft C D).comp F') (e_αₗ : αₗ = αₗ_1)
  (αᵣ αᵣ_1 : (CategoryTheory.Join.inclRight C D).comp F ⟶ (CategoryTheory.Join.inclRight C D).comp F')
  (e_αᵣ : αᵣ = αᵣ_1)
  (h :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (CategoryTheory.Join.edgeTransform C D) F)
        ((CategoryTheory.Prod.snd C D).whiskerLeft αᵣ) =
      CategoryTheory.CategoryStruct.comp ((CategoryTheory.Prod.fst C D).whiskerLeft αₗ)
        (CategoryTheory.Functor.whiskerRight (CategoryTheory.Join.edgeTransform C D) F')),
  CategoryTheory.Join.mkNatTrans αₗ αᵣ h = CategoryTheory.Join.mkNatTrans αₗ_1 αᵣ_1 ⋯
-- Init.Data.Array.Erase
Array.erase_ne_empty_iff : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {xs : Array α} {a : α}, xs.erase a ≠ #[] ↔ xs ≠ #[] ∧ xs ≠ #[a]
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
/-- The expression for `Iso.hom`.  -/
Mathlib.Tactic.BicategoryLike.Mor₂.isoHom : Lean.Expr →
  Mathlib.Tactic.BicategoryLike.IsoLift → Mathlib.Tactic.BicategoryLike.Mor₂Iso → Mathlib.Tactic.BicategoryLike.Mor₂
-- Mathlib.Order.Hom.Bounded
BoundedOrderHomClass.toTopHomClass : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : LE α] [inst_2 : LE β]
  [inst_3 : BoundedOrder α] [inst_4 : BoundedOrder β] [BoundedOrderHomClass F α β], TopHomClass F α β
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.L1.integral_of_fun_eq_integral : ∀ {α : Type u_1} {G : Type u_5} [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ℝ G] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {f : α → G} (hf : MeasureTheory.Integrable f μ),
  ∫ (a : α), ↑↑(MeasureTheory.Integrable.toL1 f hf) a ∂μ = ∫ (a : α), f a ∂μ
-- Mathlib.CategoryTheory.Sites.EffectiveEpimorphic
/-- Implementation: This is a construction which will be used in the proof that
the sieve generated by a family of arrows is effective epimorphic if and only if
the family is an effective epi.
 -/
CategoryTheory.isColimitOfEffectiveEpiFamilyStruct : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {B : C} →
      {α : Type u_1} →
        (X : α → C) →
          (π : (a : α) → X a ⟶ B) →
            CategoryTheory.EffectiveEpiFamilyStruct X π →
              CategoryTheory.Limits.IsColimit (CategoryTheory.Sieve.generateFamily X π).arrows.cocone
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Complex.iteratedDeriv_odd_cosh : ∀ (n : ℕ), iteratedDeriv (2 * n + 1) Complex.cosh = Complex.sinh
-- Mathlib.Topology.EMetricSpace.Lipschitz
continuousOn_prod_of_subset_closure_continuousOn_lipschitzOnWith' : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : TopologicalSpace α] [inst_1 : PseudoEMetricSpace β]
  [inst_2 : PseudoEMetricSpace γ] (f : α × β → γ) {s : Set α} {t t' : Set β},
  t' ⊆ t →
    t ⊆ closure t' →
      ∀ (K : NNReal),
        (∀ a ∈ s, LipschitzOnWith K (fun y => f (a, y)) t) →
          (∀ b ∈ t', ContinuousOn (fun x => f (x, b)) s) → ContinuousOn f (s ×ˢ t)
-- Mathlib.Topology.Constructible
Topology.isConstructible_preimage_iff_of_isOpenEmbedding : ∀ {X : Type u_2} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y} {s : Set Y},
  Topology.IsOpenEmbedding f →
    IsRetrocompact (Set.range f) → s ⊆ Set.range f → (Topology.IsConstructible (f ⁻¹' s) ↔ Topology.IsConstructible s)
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.LeftFraction.map_hom_ofInv_id_assoc : ∀ {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] (W : CategoryTheory.MorphismProperty C) {X Y : C} (s : Y ⟶ X)
  (hs : W s) (L : CategoryTheory.Functor C D) (hL : W.IsInvertedBy L) {Z : D} (h : L.obj Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (L.map s)
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.MorphismProperty.LeftFraction.ofInv s hs).map L hL) h) =
    h
-- Mathlib.Algebra.GroupWithZero.Indicator
Set.indicator_mul_right : ∀ {ι : Type u_1} {M₀ : Type u_4} [inst : MulZeroClass M₀] {i : ι} (s : Set ι) (f g : ι → M₀),
  s.indicator (fun j => f j * g j) i = f i * s.indicator g i
-- Mathlib.NumberTheory.Padics.HeightOneSpectrum
IsIntegralClosure.equiv.eq_1 : ∀ (R : Type u_1) (A : Type u_2) (B : Type u_3) [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : CommRing B]
  [inst_3 : Algebra R B] [inst_4 : Algebra A B] [inst_5 : IsIntegralClosure A R B] (A' : Type u_4)
  [inst_6 : CommRing A'] [inst_7 : Algebra A' B] [inst_8 : IsIntegralClosure A' R B] [inst_9 : Algebra R A]
  [inst_10 : Algebra R A'] [inst_11 : IsScalarTower R A B] [inst_12 : IsScalarTower R A' B],
  IsIntegralClosure.equiv R A B A' =
    AlgEquiv.ofAlgHom (IsIntegralClosure.lift R A' B) (IsIntegralClosure.lift R A B) ⋯ ⋯
-- Mathlib.RingTheory.Radical.NatInt
Nat.radical_le_self_iff : ∀ {n : ℕ}, UniqueFactorizationMonoid.radical n ≤ n ↔ n ≠ 0
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax
/-- Lax unity.  -/
CategoryTheory.Lax.LaxTrans.naturality_id_assoc : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.LaxFunctor B C} (self : CategoryTheory.Lax.LaxTrans F G) (a : B) {Z : F.obj a ⟶ G.obj a}
  (h : CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.CategoryStruct.id a)) (self.app a) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (self.app a) (G.mapId a))
      (CategoryTheory.CategoryStruct.comp (self.naturality (CategoryTheory.CategoryStruct.id a)) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor (self.app a)).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor (self.app a)).inv
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapId a) (self.app a)) h))
-- Mathlib.CategoryTheory.Elements
CategoryTheory.CategoryOfElements.costructuredArrowULiftYonedaEquivalence_counitIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor Cᵒᵖ (Type (max w v))),
  (CategoryTheory.CategoryOfElements.costructuredArrowULiftYonedaEquivalence F).counitIso =
    CategoryTheory.NatIso.ofComponents
      (fun X =>
        CategoryTheory.CostructuredArrow.isoMk
          (CategoryTheory.Iso.refl
            (({ obj := fun X => Opposite.op (F.elementsMk (Opposite.op X.left) (CategoryTheory.uliftYonedaEquiv X.hom)),
                        map := fun {X Y} f =>
                          (CategoryTheory.CategoryOfElements.homMk
                              (F.elementsMk (Opposite.op Y.left) (CategoryTheory.uliftYonedaEquiv Y.hom))
                              (F.elementsMk (Opposite.op X.left) (CategoryTheory.uliftYonedaEquiv X.hom)) f.left.op
                              ⋯).op,
                        map_id := ⋯, map_comp := ⋯ }.comp
                    {
                      obj := fun x =>
                        CategoryTheory.CostructuredArrow.mk
                          (CategoryTheory.uliftYonedaEquiv.symm (Opposite.unop x).snd),
                      map := fun {X Y} f => CategoryTheory.CostructuredArrow.homMk (↑(Opposite.unop f)).unop ⋯,
                      map_id := ⋯, map_comp := ⋯ }).obj
                X).left)
          ⋯)
      ⋯
-- Mathlib.Dynamics.SymbolicDynamics.Basic
SymbolicDynamics.FullShift.mulFullShift.eq_1 : ∀ (A : Type u_1) (G : Type u_2) [inst : TopologicalSpace A] [inst_1 : Monoid G],
  SymbolicDynamics.FullShift.mulFullShift A G = { carrier := Set.univ, isClosed := ⋯, mapsTo := ⋯ }
-- Mathlib.Data.Nat.PrimeFin
Nat.pos_of_mem_primeFactors : ∀ {n p : ℕ}, p ∈ n.primeFactors → 0 < p
-- Init.Data.String.Pattern.String
String.Slice.Pattern.ForwardSliceSearcher.instFiniteIdSearchStep : ∀ {s : String.Slice}, Std.Iterators.Finite (String.Slice.Pattern.ForwardSliceSearcher s) Id
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
/-- If `f b = 1`, then the product of `f a` with `a ∈ s` is the same as the product of `f a` for
`a ∈ s ∖ {b}`.  -/
tprod_eq_tprod_sdiff_singleton : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α} (s : Set β) {b : β},
  f b = 1 → ∏' (a : ↑s), f ↑a = ∏' (a : ↑(s \ {b})), f ↑a
-- Mathlib.CategoryTheory.Limits.Shapes.End
/-- The shape of multiequalizer diagrams involved in the definition of ends.  -/
CategoryTheory.Limits.multicospanShapeEnd : (J : Type u) → [CategoryTheory.Category.{v, u} J] → CategoryTheory.Limits.MulticospanShape