mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Notation.Support
Pi.mulSupport_mulSingle_of_ne : ∀ {ι : Type u_1} {M : Type u_3} [inst : DecidableEq ι] [inst_1 : One M] {i : ι} {a : M},
  a ≠ 1 → Function.mulSupport (Pi.mulSingle i a) = {i}
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.yonedaEquiv_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} {F G : CategoryTheory.Functor Cᵒᵖ (Type v₁)}
  (α : CategoryTheory.yoneda.obj X ⟶ F) (β : F ⟶ G),
  CategoryTheory.yonedaEquiv (CategoryTheory.CategoryStruct.comp α β) =
    (CategoryTheory.ConcreteCategory.hom (β.app (Opposite.op X))) (CategoryTheory.yonedaEquiv α)
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.subgraphOfAdj_symm : ∀ {V : Type u} {G : SimpleGraph V} {v w : V} (hvw : G.Adj v w), G.subgraphOfAdj ⋯ = G.subgraphOfAdj hvw
-- Init.Data.List.Lemmas
List.ne_nil_of_mem : ∀ {α : Type u_1} {a : α} {l : List α}, a ∈ l → l ≠ []
-- Mathlib.Algebra.Module.SpanRank
/-- For a finitely generated submodule, its spanRank is less than or equal to a cardinal `a`
if and only if there is a generating subset with cardinality less than or equal to `a`.  -/
Submodule.FG.spanRank_le_iff_exists_span_set_card_le : ∀ {R : Type u_1} {M : Type u} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (p : Submodule R M)
  {a : Cardinal.{u}}, p.spanRank ≤ a ↔ ∃ s, Cardinal.mk ↑s ≤ a ∧ Submodule.span R s = p
-- Mathlib.CategoryTheory.Monoidal.Limits.Shapes.Pullback
CategoryTheory.MonoidalCategory.Limits.pushout.condition_whiskerRight : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Limits.HasPushouts C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} {Q : C},
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Q)
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.pushout.inl f g) Q) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight g Q)
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.pushout.inr f g) Q)
-- Mathlib.Tactic.ClickSuggestions.ApplyAt
/-- How many new goals are generated.  -/
Mathlib.Tactic.ClickSuggestions.ApplyAtKey.numGoals : Mathlib.Tactic.ClickSuggestions.ApplyAtKey → ℕ
-- Mathlib.Algebra.Algebra.Spectrum.Basic
spectrum.setOfPred_isUnit_inter_mul_comm : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Ring A] [inst_2 : Algebra R A] (a b : A),
  {r | IsUnit r} ∩ spectrum R (a * b) = {r | IsUnit r} ∩ spectrum R (b * a)
-- Mathlib.Data.Set.Prod
Set.diagonal_eq_univ_iff : ∀ {α : Type u_1}, Set.diagonal α = Set.univ ↔ Subsingleton α
-- Mathlib.Combinatorics.SimpleGraph.UnitDistance.Basic
SimpleGraph.UnitDistEmbedding.embed_p_apply : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} {E : Type u_3} [inst : MetricSpace E]
  (U : G.UnitDistEmbedding E) (f : H ↪g G) (a : W), (U.embed f).p a = U.p (f.toCopy.toEmbedding a)
-- Mathlib.Data.Prod.Basic
Prod.fst_comp_mk : ∀ {α : Type u_1} {β : Type u_2} (x : α), Prod.fst ∘ Prod.mk x = Function.const β x
-- Mathlib.Data.Set.Lattice
Set.BijOn.iInter_congr : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set β} {t : Set γ} (f : β → Set α) (g : γ → Set α) {h : β → γ},
  Set.BijOn h s t → (∀ (x : β), g (h x) = f x) → ⋂ x ∈ s, f x = ⋂ y ∈ t, g y
-- Init.Data.UInt.Lemmas
UInt32.toFin_ofNatTruncate_of_lt : ∀ {n : ℕ} (hn : n < UInt32.size), (UInt32.ofNatClamp n).toFin = ⟨n, hn⟩
-- Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
/-- **Vitali-Carathéodory Theorem**: given an integrable real function `f`, there exists an
integrable function `g > f` which is lower semicontinuous, with integral arbitrarily close
to that of `f`. This function has to be `EReal`-valued in general.  -/
MeasureTheory.exists_lt_lowerSemicontinuous_integral_lt : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] [BorelSpace α] {μ : MeasureTheory.Measure α}
  [μ.WeaklyRegular] [MeasureTheory.SigmaFinite μ] (f : α → ℝ),
  MeasureTheory.Integrable f μ →
    ∀ {ε : ℝ},
      0 < ε →
        ∃ g,
          (∀ (x : α), ↑(f x) < g x) ∧
            LowerSemicontinuous g ∧
              MeasureTheory.Integrable (fun x => (g x).toReal) μ ∧
                (∀ᵐ (x : α) ∂μ, g x < ⊤) ∧ ∫ (x : α), (g x).toReal ∂μ < ∫ (x : α), f x ∂μ + ε
-- Mathlib.Topology.Convenient.Category
GeneratedByTopCat.instCoeSortType : {ι : Type t} → (X : ι → Type u) → [inst : (i : ι) → TopologicalSpace (X i)] → CoeSort (GeneratedByTopCat X) (Type v)
-- Mathlib.Algebra.Category.Ring.Colimits
CommRingCat.Colimits.Prequotient.add.injEq : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CommRingCat}
  (a a_1 a_2 a_3 : CommRingCat.Colimits.Prequotient F), (a.add a_1 = a_2.add a_3) = (a = a_2 ∧ a_1 = a_3)
-- Mathlib.Data.ENat.BigOperators
ENat.exists_le_of_sum_le : ∀ {α : Type u_1} {s : Finset α}, s.Nonempty → ∀ {f g : α → ℕ∞}, ∑ i ∈ s, f i ≤ ∑ i ∈ s, g i → ∃ i ∈ s, f i ≤ g i
-- Mathlib.Topology.Algebra.Module.Alternating.Topology
ContinuousLinearEquiv.continuousAlternatingMapCongr_apply : ∀ {𝕜 : Type u_1} {E : Type u_2} {E' : Type u_3} {F : Type u_4} {G : Type u_5} {ι : Type u_6} [inst : NormedField 𝕜]
  [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E] [inst_3 : TopologicalSpace E] [inst_4 : AddCommGroup E']
  [inst_5 : Module 𝕜 E'] [inst_6 : TopologicalSpace E'] [inst_7 : AddCommGroup F] [inst_8 : Module 𝕜 F]
  [inst_9 : TopologicalSpace F] [inst_10 : IsTopologicalAddGroup F] [inst_11 : ContinuousConstSMul 𝕜 F]
  [inst_12 : AddCommGroup G] [inst_13 : Module 𝕜 G] [inst_14 : TopologicalSpace G] [inst_15 : IsTopologicalAddGroup G]
  [inst_16 : ContinuousConstSMul 𝕜 G] (e : E ≃L[𝕜] E') (e' : F ≃L[𝕜] G) (x : E [⋀^ι]→L[𝕜] F),
  (e.continuousAlternatingMapCongr e') x = (↑e').compContinuousAlternatingMap (x.compContinuousLinearMap ↑e.symm)
-- Mathlib.RingTheory.IntegralClosure.IntegralRestrict
galLift_comp : ∀ {A : Type u_1} (K : Type u_2) (L : Type u_3) (L₂ : Type u_4) (L₃ : Type u_5) {B : Type u_6} {B₂ : Type u_7}
  {B₃ : Type u_8} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : CommRing B₂] [inst_3 : CommRing B₃]
  [inst_4 : Algebra A B] [inst_5 : Algebra A B₂] [inst_6 : Algebra A B₃] [inst_7 : Field K] [inst_8 : Field L]
  [inst_9 : Field L₂] [inst_10 : Field L₃] [inst_11 : Algebra A K] [inst_12 : IsFractionRing A K]
  [inst_13 : Algebra K L] [inst_14 : Algebra A L] [inst_15 : IsScalarTower A K L] [inst_16 : Algebra K L₂]
  [inst_17 : Algebra A L₂] [inst_18 : IsScalarTower A K L₂] [inst_19 : Algebra K L₃] [inst_20 : Algebra A L₃]
  [inst_21 : IsScalarTower A K L₃] [inst_22 : Algebra B L] [inst_23 : IsScalarTower A B L]
  [inst_24 : IsIntegralClosure B A L] [inst_25 : Algebra B₂ L₂] [inst_26 : IsScalarTower A B₂ L₂]
  [inst_27 : IsIntegralClosure B₂ A L₂] [inst_28 : Algebra B₃ L₃] [inst_29 : IsScalarTower A B₃ L₃]
  [inst_30 : Algebra.IsAlgebraic K L] [inst_31 : Algebra.IsAlgebraic K L₂] (σ : B →ₐ[A] B₂) (σ' : B₂ →ₐ[A] B₃),
  galLift K L L₃ (σ'.comp σ) = (galLift K L₂ L₃ σ').comp (galLift K L L₂ σ)
-- Mathlib.Topology.UniformSpace.LocallyUniformConvergence
UniformContinuous.comp_tendstoLocallyUniformly : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Type u_4} [inst : TopologicalSpace α] [inst_1 : UniformSpace β]
  {F : ι → α → β} {f : α → β} {p : Filter ι} [inst_2 : UniformSpace γ] {g : β → γ},
  UniformContinuous g → TendstoLocallyUniformly F f p → TendstoLocallyUniformly (fun x => g ∘ F x) (g ∘ f) p
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.EqCnstrProof.superpose_ac_idempotent : Lean.Grind.AC.Var → Lean.Meta.Grind.AC.EqCnstr → Lean.Meta.Grind.AC.EqCnstrProof
-- Mathlib.CategoryTheory.Sites.Descent.Precoverage
_private.Mathlib.CategoryTheory.Sites.Descent.Precoverage.0.CategoryTheory.Pseudofunctor.DescentData.full_pullFunctor.mor_unique : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} {ι : Type t} {S : C}
  {X : ι → C} {f : (i : ι) → X i ⟶ S} {ι' : Type t'} {X' : ι' → C} {f' : (j : ι') → X' j ⟶ S} {α : ι' → ι}
  {p' : (j : ι') → X' j ⟶ X (α j)} (w : ∀ (j : ι'), CategoryTheory.CategoryStruct.comp (p' j) (f (α j)) = f' j)
  {D₁ D₂ : F.DescentData f}
  (φ :
    (CategoryTheory.Pseudofunctor.DescentData.pullFunctor F ⋯).obj D₁ ⟶
      (CategoryTheory.Pseudofunctor.DescentData.pullFunctor F ⋯).obj D₂)
  ⦃i : ι⦄ {Z : C} (q : Z ⟶ X i) ⦃j₁ : ι'⦄ (a₁ : Z ⟶ X' j₁) ⦃j₂ : ι'⦄ (a₂ : Z ⟶ X' j₂)
  (fac₁ :
    autoParam (CategoryTheory.CategoryStruct.comp a₁ (f' j₁) = CategoryTheory.CategoryStruct.comp q (f i))
      CategoryTheory.Pseudofunctor.DescentData.full_pullFunctor.mor_unique._auto_1✝)
  (fac₂ :
    autoParam (CategoryTheory.CategoryStruct.comp a₂ (f' j₂) = CategoryTheory.CategoryStruct.comp q (f i))
      CategoryTheory.Pseudofunctor.DescentData.full_pullFunctor.mor_unique._auto_3✝),
  CategoryTheory.Pseudofunctor.DescentData.full_pullFunctor.mor✝ w φ q a₁ fac₁ =
    CategoryTheory.Pseudofunctor.DescentData.full_pullFunctor.mor✝ w φ q a₂ fac₂
-- Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
IsLocalFrameOn.coeff_apply_of_notMem : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → AddCommGroup (V x)] [inst_10 : (x : M) → Module 𝕜 (V x)]
  [inst_11 : (x : M) → TopologicalSpace (V x)] [inst_12 : FiberBundle F V] {ι : Type u_7} {s : ι → (x : M) → V x}
  {u : Set M} {n : WithTop ℕ∞} {x : M} (hs : IsLocalFrameOn I F n s u), x ∉ u → ∀ (i : ι), hs.coeff i x = 0
-- Mathlib.Analysis.Complex.Poisson
herglotzRieszKernel_fun_def : ∀ (c w : ℂ), herglotzRieszKernel c w = fun z => (z - c + (w - c)) / (z - c - (w - c))
-- Mathlib.CategoryTheory.Sites.CoverLifting
/-- If `G` is cocontinuous, then `G.op.ran` pushes sheaves to sheaves.

This is SGA 4 III 2.2.  -/
CategoryTheory.ran_isSheaf_of_isCocontinuous : ∀ {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] (G : CategoryTheory.Functor C D) {A : Type w}
  [inst_2 : CategoryTheory.Category.{w', w} A] {J : CategoryTheory.GrothendieckTopology C}
  (K : CategoryTheory.GrothendieckTopology D) [G.IsCocontinuous J K]
  [inst_4 : ∀ (F : CategoryTheory.Functor Cᵒᵖ A), G.op.HasPointwiseRightKanExtension F] (ℱ : CategoryTheory.Sheaf J A),
  CategoryTheory.Presheaf.IsSheaf K (G.op.ran.obj ℱ.obj)
-- Lean.Environment
/-- Accessibility levels of declarations in `Lean.Environment`.  -/
Lean.Environment.Visibility : Type
-- Mathlib.Algebra.Algebra.Basic
/-- Semiring ⥤ ℕ-Alg  -/
Semiring.toNatAlgebra : {R : Type u_1} → [inst : Semiring R] → Algebra ℕ R
-- Mathlib.CategoryTheory.Monoidal.Mod
/-- The action map  -/
CategoryTheory.MonObj.«termγ[_]» : Lean.ParserDescr
-- Mathlib.Topology.Algebra.Algebra
ContinuousAlgHom.map_neg : ∀ (R : Type u_1) [inst : CommSemiring R] {S : Type u_3} [inst_1 : Ring S] [inst_2 : TopologicalSpace S]
  [inst_3 : Algebra R S] {B : Type u_4} [inst_4 : Ring B] [inst_5 : TopologicalSpace B] [inst_6 : Algebra R B]
  (f : S →A[R] B) (x : S), f (-x) = -f x
-- Lean.Expr
Lean.Int.mkInstLE : Lean.Expr
-- Mathlib.Order.Filter.Pointwise
Filter.isUnit_iff : ∀ {α : Type u_2} [inst : DivisionMonoid α] {f : Filter α}, IsUnit f ↔ ∃ a, f = pure a ∧ IsUnit a
-- Mathlib.CategoryTheory.Sites.JointlySurjective
/-- The pullback of the jointly surjective precoverage of types to any category `C` via a
(forgetful) functor `C ⥤ Type u` is stable under base change if the canonical map
`F (X ×[Y] Z) ⟶ F(X) ×[F(Y)] F(Z)` is surjective.  -/
CategoryTheory.isStableUnderBaseChange_comap_jointlySurjectivePrecoverage : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (F : CategoryTheory.Functor C (Type u)),
  (∀ {X Y S : C} (f : X ⟶ S) (g : Y ⟶ S) [inst_1 : CategoryTheory.Limits.HasPullback f g],
      Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pullbackComparison F f g))) →
    (CategoryTheory.Precoverage.comap F CategoryTheory.Types.jointlySurjectivePrecoverage).IsStableUnderBaseChange
-- Mathlib.Combinatorics.Young.YoungDiagram
YoungDiagram.ext : ∀ {x y : YoungDiagram}, x.cells = y.cells → x = y
-- Mathlib.Analysis.Normed.Group.Constructions
Pi.seminormedAddCommGroup.eq_1 : ∀ {ι : Type u_1} {G : ι → Type u_4} [inst : Fintype ι] [inst_1 : (i : ι) → SeminormedAddCommGroup (G i)],
  Pi.seminormedAddCommGroup =
    { toNorm := Pi.seminormedAddGroup.toNorm, toAddGroup := Pi.seminormedAddGroup.toAddGroup, add_comm := ⋯,
      toPseudoMetricSpace := Pi.seminormedAddGroup.toPseudoMetricSpace, dist_eq := ⋯ }
-- Mathlib.SetTheory.ZFC.Class
/-- Function value  -/
Class.fval : Class.{u} → Class.{u} → Class.{u}
-- Mathlib.RingTheory.HahnSeries.Binomial
HahnSeries.SummableFamily.binomialFamily.eq_1 : ∀ {Γ : Type u_1} {R : Type u_2} {A : Type u_3} [inst : LinearOrder Γ] [inst_1 : AddCommMonoid Γ]
  [inst_2 : IsOrderedCancelAddMonoid Γ] [inst_3 : CommRing R] [inst_4 : BinomialRing R] [inst_5 : CommRing A]
  [inst_6 : Algebra R A] (x : HahnSeries Γ A) (r : R),
  HahnSeries.SummableFamily.binomialFamily x r =
    HahnSeries.SummableFamily.powerSeriesFamily (x - 1) (PowerSeries.binomialSeries A r)
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.coneUnopOfCoconeEquiv_unitIso : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ},
  CategoryTheory.Limits.coneUnopOfCoconeEquiv.unitIso =
    CategoryTheory.Iso.refl (CategoryTheory.Functor.id (CategoryTheory.Limits.Cocone F)ᵒᵖ)
-- Aesop.BuiltinRules.Assumption
Aesop.BuiltinRules.assumption : Aesop.RuleTac
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.getKey_alter_self : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp]
  [Inhabited α],
  t.WF →
    ∀ {k : α} {f : Option β → Option β} {hc : k ∈ Std.DTreeMap.Raw.Const.alter t k f},
      (Std.DTreeMap.Raw.Const.alter t k f).getKey k hc = k
-- Mathlib.Algebra.Ring.Subsemiring.Defs
Subsemiring.coe_mk' : ∀ {R : Type u} [inst : NonAssocSemiring R] (s : Set R) (sm : Submonoid R) (hm : ↑sm = s) (sa : AddSubmonoid R)
  (ha : ↑sa = s), ↑(Subsemiring.mk' s sm hm sa ha) = s
-- Mathlib.RepresentationTheory.Rep.Res
/-- A `G`-representation `A` on which a normal subgroup `S ≤ G` acts trivially induces a
`G ⧸ S`-representation on `A`, and composing this with the quotient map `G → G ⧸ S` gives the
original representation by definition. Useful for typechecking.  -/
Rep.resOfQuotientIso : {k : Type u} →
  [inst : Semiring k] →
    {G : Type v} →
      [inst_1 : Group G] →
        (A : Rep.{u_1, u, v} k G) →
          (S : Subgroup G) →
            [inst_2 : S.Normal] →
              [inst_3 : Representation.IsTrivial (MonoidHom.comp A.ρ S.subtype)] →
                Rep.res (QuotientGroup.mk' S) (A.ofQuotient S) ≅ A
-- Mathlib.Analysis.Complex.ReImTopology
/-- **Alias** of `Complex.closure_setOfPred_lt_im`. -/
Complex.closure_setOf_lt_im : ∀ (a : ℝ), closure {z | a < z.im} = {z | a ≤ z.im}
-- Mathlib.LinearAlgebra.Matrix.HadamardMatrix
/-- Build a Hadamard matrix from the one-sided row-orthogonality condition, provided the order is
regular in `R`.

This is the matrix form of [Theorem 2.3.6][deLauneyFlannery2011].  -/
Matrix.IsHadamard.of_mul_conjTranspose : ∀ {n : Type u_2} {R : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing R] [inst_3 : StarRing R]
  {A : Matrix n n R},
  (∀ (i j : n), A i j ∈ unitary R) →
    A * A.conjTranspose = ↑(Fintype.card n) • 1 → IsRegular ↑(Fintype.card n) → A.IsHadamard
-- Mathlib.AlgebraicTopology.SimplexCategory.SemiSimplexCategory
SemiSimplexCategory.homEquiv_comp : ∀ {a b c : SemiSimplexCategory} (f : a ⟶ b) (g : b ⟶ c),
  SemiSimplexCategory.homEquiv (CategoryTheory.CategoryStruct.comp f g) =
    RelEmbedding.trans (SemiSimplexCategory.homEquiv f) (SemiSimplexCategory.homEquiv g)
-- Lean.Meta.Diagnostics
Lean.Meta.DiagSummary.max : Lean.Meta.DiagSummary → ℕ
-- Init.Data.String.Decode
String.utf8EncodeChar_eq_cons_cons_cons : ∀ {c : Char},
  c.utf8Size = 3 →
    String.utf8EncodeChar c =
      [(c.val >>> 12).toUInt8 &&& 15 ||| 224, (c.val >>> 6).toUInt8 &&& 63 ||| 128, c.val.toUInt8 &&& 63 ||| 128]
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
MeasureTheory.AEStronglyMeasurable.neg : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {m m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {f : α → β} [inst_1 : Neg β] [ContinuousNeg β],
  MeasureTheory.AEStronglyMeasurable f μ → MeasureTheory.AEStronglyMeasurable (-f) μ
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
/-- If the colimit of `F` exists and `G` preserves it, then if `G` reflects isomorphisms then it
reflects the colimit of `F` (see also `JointlyReflectIsomorphisms.jointlyReflectsLimit` in
the file `CategoryTheory/Functor/ReflectsIso/Limits.lean` for the corresponding result
for a family of functors which joinly reflect isomorphisms).
 -/
CategoryTheory.Limits.reflectsColimit_of_reflectsIsomorphisms : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J] (F : CategoryTheory.Functor J C)
  (G : CategoryTheory.Functor C D) [G.ReflectsIsomorphisms] [CategoryTheory.Limits.HasColimit F]
  [CategoryTheory.Limits.PreservesColimit F G], CategoryTheory.Limits.ReflectsColimit F G
-- Mathlib.Algebra.Star.Pointwise
Set.star_subset : ∀ {α : Type u_1} [inst : InvolutiveStar α] {s t : Set α}, star s ⊆ t ↔ s ⊆ star t
-- Init.Data.List.Scan.Lemmas
List.scanr_nil : ∀ {α : Type u_1} {β : Type u_2} {init : β} {f : α → β → β}, List.scanr f init [] = [init]
-- Mathlib.Topology.LocallyConstant.Algebra
/-- `DFunLike.coe` as a `MonoidHom`.  -/
LocallyConstant.coeFnMonoidHom : {X : Type u_1} → {Y : Type u_2} → [inst : TopologicalSpace X] → [inst_1 : MulOneClass Y] → LocallyConstant X Y →* X → Y
-- Mathlib.ModelTheory.Syntax
/-- `BoundedFormula α n` is the type of formulas with free variables indexed by `α` and `n` in-scope
bound variables indexed by `Fin n`.  -/
FirstOrder.Language.BoundedFormula : FirstOrder.Language → Type u' → ℕ → Type (max u v u')
-- Lean.Compiler.IR.Basic
Lean.IR.IRType.isObj : Lean.IR.IRType → Bool
-- Mathlib.Algebra.Order.Group.OrderIso
OrderIso.mulRight_toEquiv : ∀ {α : Type u} [inst : Group α] [inst_1 : LE α] [inst_2 : MulRightMono α] (a : α),
  (OrderIso.mulRight a).toEquiv = Equiv.mulRight a
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
/-- Convert a multiseries in a non-empty basis to a sequence of pairs `(exp, coef)`.  -/
Tactic.ComputeAsymptotics.MultiseriesExpansion.seq : {basis_hd : ℝ → ℝ} →
  {basis_tl : List (ℝ → ℝ)} →
    Tactic.ComputeAsymptotics.MultiseriesExpansion (basis_hd :: basis_tl) →
      Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl
-- Batteries.Recycling.RBTree.Basic
/-- `path.erase t v` removes the root element of `t` from the tree, assuming that `(t, path)` was
the result of a previous `zoom` operation.
 -/
RBTree.RBNode.Path.erase : {α : Type u_1} → RBTree.RBNode.Path α → RBTree.RBNode α → RBTree.RBNode α
-- Init.Data.SInt.Lemmas
ISize.ofNat_mod : ∀ {a b : ℕ},
  a < 2 ^ (System.Platform.numBits - 1) →
    b < 2 ^ (System.Platform.numBits - 1) → ISize.ofNat (a % b) = ISize.ofNat a % ISize.ofNat b
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Equiv.diff_right : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ m₃ : Std.DHashMap α β} [EquivBEq α]
  [LawfulHashable α], m₂.Equiv m₃ → (m₁ \ m₂).Equiv (m₁ \ m₃)
-- Mathlib.Tactic.FunProp.Core
/-- Try to apply theorem - core function  -/
Mathlib.Meta.FunProp.tryTheoremCore : Array Lean.Expr →
  Lean.Expr →
    Lean.Expr →
      Lean.Expr →
        Mathlib.Meta.FunProp.Origin →
          (Lean.Expr → Mathlib.Meta.FunProp.FunPropM (Option Mathlib.Meta.FunProp.Result)) →
            Mathlib.Meta.FunProp.FunPropM (Option Mathlib.Meta.FunProp.Result)
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
/-- The first part of the third simplicial identity  -/
CategoryTheory.SimplicialObject.δ_comp_σ_self_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject C) {n : ℕ}
  {i : Fin (n + 1)} {Z : C} (h : X.obj (Opposite.op { len := n }) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.σ i) (CategoryTheory.CategoryStruct.comp (X.δ i.castSucc) h) = h
-- Init.Data.String.Basic
String.Pos.Raw.prev_zero : ∀ (s : String), String.Pos.Raw.prev s 0 = 0
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
CochainComplex.mappingCone.ext_to_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] (i j : ℤ) (hij : i + 1 = j)
  {A : C} (f g : A ⟶ (CochainComplex.mappingCone φ).X i),
  f = g ↔
    CategoryTheory.CategoryStruct.comp f ((↑(CochainComplex.mappingCone.fst φ)).v i j hij) =
        CategoryTheory.CategoryStruct.comp g ((↑(CochainComplex.mappingCone.fst φ)).v i j hij) ∧
      CategoryTheory.CategoryStruct.comp f ((CochainComplex.mappingCone.snd φ).v i i ⋯) =
        CategoryTheory.CategoryStruct.comp g ((CochainComplex.mappingCone.snd φ).v i i ⋯)
-- Mathlib.CategoryTheory.Limits.Constructions.Over.Connected
/-- The forgetful functor from the over category preserves any connected limit.  -/
CategoryTheory.Over.preservesLimitsOfShape_forget_of_isConnected : ∀ {J : Type u'} [inst : CategoryTheory.Category.{v', u'} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  [CategoryTheory.IsConnected J] {B : C}, CategoryTheory.Limits.PreservesLimitsOfShape J (CategoryTheory.Over.forget B)
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.eLpNorm'_const_of_isProbabilityMeasure : ∀ {α : Type u_1} {ε : Type u_2} {m0 : MeasurableSpace α} {q : ℝ} {μ : MeasureTheory.Measure α} [inst : ENorm ε] (c : ε),
  0 < q → ∀ [MeasureTheory.IsProbabilityMeasure μ], MeasureTheory.eLpNorm' (fun x => c) q μ = ‖c‖ₑ
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.coeff_one_X : ∀ {R : Type u_1} [inst : Semiring R], (PowerSeries.coeff 1) PowerSeries.X = 1
-- Mathlib.Logic.Equiv.Defs
/-- Equivalence between `Fin 1` and `Unit`.  -/
finOneEquiv : Fin 1 ≃ Unit
-- Mathlib.Analysis.Calculus.ContDiff.Basic
/-- A function is `C^k` on two open sets iff it is `C^k` on their union.  -/
contDiffOn_union_iff_of_isOpen : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s t : Set E} {f : E → F}
  {n : WithTop ℕ∞}, IsOpen s → IsOpen t → (ContDiffOn 𝕜 n f (s ∪ t) ↔ ContDiffOn 𝕜 n f s ∧ ContDiffOn 𝕜 n f t)
-- Aesop.Rule.Name
Aesop.BuilderName : Type
-- Mathlib.Algebra.BigOperators.Fin
Fin.partialSum_succ : ∀ {M : Type u_2} [inst : AddMonoid M] {n : ℕ} (f : Fin n → M) (j : Fin n),
  Fin.partialSum f j.succ = Fin.partialSum f j.castSucc + f j
-- Mathlib.MeasureTheory.Measure.WithDensity
MeasureTheory.withDensity_ofReal_mutuallySingular : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ},
  Measurable f →
    (μ.withDensity fun x => ENNReal.ofReal (f x)).MutuallySingular (μ.withDensity fun x => ENNReal.ofReal (-f x))
-- Mathlib.Tactic.NormNum.Result
Mathlib.Meta.NormNum.instInhabitedResult' : Inhabited Mathlib.Meta.NormNum.Result'
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.maxKeyD_insertIfNew : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k : α} {v : β k}
  {fallback : α},
  (t.insertIfNew k v).maxKeyD fallback = t.maxKey?.elim k fun k' => if cmp k' k = Ordering.lt then k else k'
-- Mathlib.Data.NNReal.Basic
NNReal.image_coe_Ioo : ∀ (x y : NNReal), NNReal.toReal '' Set.Ioo x y = Set.Ioo ↑x ↑y
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.tan_nonneg_of_nonneg_of_le_pi_div_two : ∀ {x : ℝ}, 0 ≤ x → x ≤ Real.pi / 2 → 0 ≤ Real.tan x