mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.ShrinkYoneda
CategoryTheory.shrinkCoyonedaObjObjEquiv_map_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C] {X X' : Cᵒᵖ}
  {Y : C} (f : (CategoryTheory.shrinkCoyoneda.{w, v, u}.obj X).obj Y) (g : X ⟶ X'),
  CategoryTheory.shrinkCoyonedaObjObjEquiv
      ((CategoryTheory.ConcreteCategory.hom ((CategoryTheory.shrinkCoyoneda.{w, v, u}.map g).app Y)) f) =
    CategoryTheory.CategoryStruct.comp g.unop (CategoryTheory.shrinkCoyonedaObjObjEquiv f)
-- Mathlib.Algebra.Group.AddChar
MonoidHom.coe_compAddChar : ∀ {A : Type u_1} {M : Type u_3} [inst : AddMonoid A] [inst_1 : Monoid M] {N : Type u_5} [inst_2 : Monoid N] (f : M →* N)
  (φ : AddChar A M), ⇑(f.compAddChar φ) = ⇑f ∘ ⇑φ
-- Mathlib.LinearAlgebra.TensorAlgebra.Basic
TensorAlgebra.algebraMap_eq_one_iff : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Type u_2) [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (x : R),
  (algebraMap R (TensorAlgebra R M)) x = 1 ↔ x = 1
-- Batteries.Data.Char.Basic
Char.instDecidableExistsOfDecidablePred_batteries : (P : Char → Prop) → [DecidablePred P] → Decidable (∃ c, P c)
-- Mathlib.Data.Fintype.Basic
Fin.fintype : (n : ℕ) → Fintype (Fin n)
-- Mathlib.CategoryTheory.Monoidal.Center
CategoryTheory.Center.instMonoidalCategory : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] → CategoryTheory.MonoidalCategory (CategoryTheory.Center C)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.getKey_insertMany_list_of_contains_eq_false : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] (h : (↑m).WF) {l : List (α × β)} {k : α}
  (h₁ : (List.map Prod.fst l).contains k = false)
  {h' : (↑(Std.DHashMap.Internal.Raw₀.Const.insertMany m l)).contains k = true},
  (↑(Std.DHashMap.Internal.Raw₀.Const.insertMany m l)).getKey k h' = m.getKey k ⋯
-- Mathlib.Order.SuccPred.Basic
/-- **Alias** of the forward direction of `Order.pred_lt_pred_iff`. -/
Order.lt_of_pred_lt_pred : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : PredOrder α] {a b : α} [NoMinOrder α],
  Order.pred b < Order.pred a → b < a
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
mul_lt_mul_of_lt_of_le : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Preorder α] [MulLeftMono α] [MulRightStrictMono α] {a b c d : α},
  a < b → c ≤ d → a * c < b * d
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
Measurable.eval : ∀ {α : Type u_1} {δ : Type u_4} {X : δ → Type u_6} [inst : MeasurableSpace α] [inst_1 : (a : δ) → MeasurableSpace (X a)]
  {a : δ} {g : α → (a : δ) → X a}, Measurable g → Measurable fun x => g x a
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.isBoundedSMulSeminormedAddCommGroupToPi : ∀ (p : ENNReal) {ι : Type u_2} (α : ι → Type u_3) [inst : Fact (1 ≤ p)] [inst_1 : Fintype ι]
  [inst_2 : (i : ι) → SeminormedAddCommGroup (α i)] {R : Type u_5} [inst_3 : SeminormedRing R]
  [inst_4 : (i : ι) → Module R (α i)] [∀ (i : ι), IsBoundedSMul R (α i)], IsBoundedSMul R ((i : ι) → α i)
-- Mathlib.Combinatorics.SetFamily.Shadow
/-- The shadow is monotone.  -/
Finset.shadow_monotone : ∀ {α : Type u_1} [inst : DecidableEq α], Monotone Finset.shadow
-- Mathlib.Algebra.MvPolynomial.Degrees
MvPolynomial.degreeOf_add_eq_of_degreeOf_lt : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {p q : MvPolynomial σ R} {i : σ},
  MvPolynomial.degreeOf i q < MvPolynomial.degreeOf i p → MvPolynomial.degreeOf i (p + q) = MvPolynomial.degreeOf i p
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.exists_pos_measure_of_not_restrict_le_zero : ∀ {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : AddCommMonoid M]
  [inst_2 : LinearOrder M] (v : MeasureTheory.VectorMeasure α M) {i : Set α},
  ¬v.restrict i ≤ MeasureTheory.VectorMeasure.restrict 0 i → ∃ j, MeasurableSet j ∧ j ⊆ i ∧ 0 < v j
-- Mathlib.Topology.MetricSpace.Lipschitz
LipschitzWith.dist_right : ∀ {α : Type u} [inst : PseudoMetricSpace α] (x : α), LipschitzWith 1 (dist x)
-- Std.Tactic.Do.Syntax
Lean.Parser.Tactic.MCasesPat.stateful.sizeOf_spec : ∀ (h : Lean.TSyntax `Lean.binderIdent), sizeOf (Lean.Parser.Tactic.MCasesPat.stateful h) = 1 + sizeOf h
-- Mathlib.Combinatorics.Matroid.Map
/-- Map `M : Matroid α` to a `Matroid β` with ground set `E` using an equivalence `M.E ≃ E`.
Defined using `Matroid.ofExistsMatroid` for better defeq.  -/
Matroid.mapSetEquiv : {α : Type u_1} → {β : Type u_2} → (M : Matroid α) → {E : Set β} → ↑M.E ≃ ↑E → Matroid β
-- Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
ContMDiffSection.coe_neg : ∀ {𝕜 : 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] {n : WithTop ℕ∞} {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → TopologicalSpace (V x)] [inst_10 : FiberBundle F V] [inst_11 : (x : M) → AddCommGroup (V x)]
  [inst_12 : (x : M) → Module 𝕜 (V x)] [inst_13 : VectorBundle 𝕜 F V] (s : ContMDiffSection I F n V), ⇑(-s) = -⇑s
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
isOpen_extChartAt_preimage : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  {I : ModelWithCorners 𝕜 E H} [inst_5 : ChartedSpace H M] (x : M) {s : Set E},
  IsOpen s → IsOpen ((chartAt H x).source ∩ ↑(extChartAt I x) ⁻¹' s)
-- Mathlib.RingTheory.OreLocalization.NonZeroDivisors
/-- The inversion of Ore fractions for a ring without zero divisors, satisfying `0⁻¹ = 0` and
`(r /ₒ r')⁻¹ = r' /ₒ r` for `r ≠ 0`.  -/
OreLocalization.inv : {R : Type u_1} →
  [inst : MonoidWithZero R] →
    [Nontrivial R] →
      [inst_2 : OreLocalization.OreSet (nonZeroDivisors R)] →
        [NoZeroDivisors R] → OreLocalization (nonZeroDivisors R) R → OreLocalization (nonZeroDivisors R) R
-- Mathlib.Order.BooleanAlgebra.Basic
compl_inf : ∀ {α : Type u} {x y : α} [inst : BooleanAlgebra α], (x ⊓ y)ᶜ = xᶜ ⊔ yᶜ
-- Mathlib.MeasureTheory.Group.Convolution
MeasureTheory.Measure.map_conv_addMonoidHom : ∀ {M : Type u_2} {M' : Type u_3} {mM : MeasurableSpace M} [inst : AddMonoid M] [MeasurableAdd₂ M]
  {mM' : MeasurableSpace M'} [inst_2 : AddMonoid M'] [MeasurableAdd₂ M'] {μ ν : MeasureTheory.Measure M}
  [MeasureTheory.SFinite μ] [MeasureTheory.SFinite ν] (L : M →+ M'),
  Measurable ⇑L →
    MeasureTheory.Measure.map (⇑L) (μ.conv ν) =
      (MeasureTheory.Measure.map (⇑L) μ).conv (MeasureTheory.Measure.map (⇑L) ν)
-- Mathlib.FieldTheory.AlgebraicClosure
/-- If `E` is algebraically closed, then the algebraic closure of `F` in `E` is an absolute
algebraic closure of `F`.  -/
algebraicClosure.isAlgClosure : ∀ (F : Type u_1) (E : Type u_2) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] [IsAlgClosed E],
  IsAlgClosure F ↥(algebraicClosure F E)
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
/-- How the `eisSummand` function changes under the Moebius action.  -/
EisensteinSeries.eisSummand_SL2_apply : ∀ (k : ℤ) (i : Fin 2 → ℤ) (A : Matrix.SpecialLinearGroup (Fin 2) ℤ) (z : UpperHalfPlane),
  EisensteinSeries.eisSummand k i (A • z) =
    UpperHalfPlane.denom (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) A)) ↑z ^
        k *
      EisensteinSeries.eisSummand k (Matrix.vecMul i ↑A) z
-- Mathlib.Analysis.Analytic.ChangeOrigin
FormalMultilinearSeries.derivSeries.eq_1 : ∀ {𝕜 : 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]
  (p : FormalMultilinearSeries 𝕜 E F),
  p.derivSeries = (↑↑(continuousMultilinearCurryFin1 𝕜 E F)).compFormalMultilinearSeries (p.changeOriginSeries 1)
-- Init.Data.Vector.Lemmas
Vector.anyM_toArray : ∀ {m : Type → Type u_1} {α : Type u_2} {n : ℕ} [inst : Monad m] {p : α → m Bool} {xs : Vector α n},
  Array.anyM p xs.toArray = Vector.anyM p xs
-- Mathlib.Data.ENNReal.Operations
ENNReal.image_coe_Ici : ∀ (x : NNReal), ENNReal.ofNNReal '' Set.Ici x = Set.Ico ↑x ⊤
-- Mathlib.GroupTheory.QuotientGroup.Basic
QuotientAddGroup.addEquivPiModRangeNSMulAddMonoidHom.eq_1 : ∀ {ι : Type u_1} (A : ι → Type u_2) [inst : (i : ι) → AddCommGroup (A i)] (n : ℕ),
  QuotientAddGroup.addEquivPiModRangeNSMulAddMonoidHom A n = QuotientAddGroup.liftEquiv (nsmulAddMonoidHom n).range ⋯ ⋯
-- Mathlib.MeasureTheory.Measure.Dirac
MeasureTheory.instNonemptySubtypeMeasureIsProbabilityMeasure : ∀ {α : Type u_1} [inst : MeasurableSpace α] [hα : Nonempty α], Nonempty { μ // MeasureTheory.IsProbabilityMeasure μ }
-- Mathlib.Topology.Order.LiminfLimsup
/-- The `limsInf` of a filter `f` is a cluster point of `f`.  -/
ClusterPt.limsInf : ∀ {α : Type u_2} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α]
  {f : Filter α} [f.NeBot],
  autoParam (Filter.IsCobounded (fun x1 x2 => x1 ≥ x2) f) ClusterPt.limsInf._auto_1 →
    autoParam (Filter.IsBounded (fun x1 x2 => x1 ≥ x2) f) ClusterPt.limsInf._auto_3 → ClusterPt f.limsInf f
-- Mathlib.Data.Set.Prod
Set.singleton_pi : ∀ {ι : Type u_1} {α : ι → Type u_2} (i : ι) (t : (i : ι) → Set (α i)), {i}.pi t = Function.eval i ⁻¹' t i
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
Finset.sum_const_zero : ∀ {ι : Type u_1} {M : Type u_3} {s : Finset ι} [inst : AddCommMonoid M], ∑ _x ∈ s, 0 = 0
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.contains_keysArray : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [inst : BEq α] [Std.LawfulBEqCmp cmp]
  [Std.TransCmp cmp] {k : α}, t.keysArray.contains k = t.contains k
-- Mathlib.Topology.UniformSpace.Basic
/-- Closed entourages form a basis of the uniformity filter.  -/
uniformity_hasBasis_closure : ∀ {α : Type ua} [inst : UniformSpace α], (uniformity α).HasBasis (fun V => V ∈ uniformity α) closure
-- Lean.Meta.Basic
/-- Execute `x` allowing `isDefEq` to assign synthetic opaque metavariables.  -/
Lean.Meta.withAssignableSyntheticOpaque : {n : Type → Type u_1} → [MonadControlT Lean.MetaM n] → [Monad n] → {α : Type} → n α → n α
-- Lean.Message
Lean.instFromJsonBaseMessage.fromJson : {α : Type} → [Lean.FromJson α] → Lean.Json → Except String (Lean.BaseMessage α)
-- Mathlib.LinearAlgebra.BilinearForm.Properties
/-- The `B`-dual basis `B.dualBasis hB b` to a finite basis `b` satisfies
`B (B.dualBasis hB b i) (b j) = B (b i) (B.dualBasis hB b j) = if i = j then 1 else 0`,
where `B` is a nondegenerate (symmetric) bilinear form and `b` is a finite basis.  -/
LinearMap.BilinForm.dualBasis : {V : Type u_5} →
  {K : Type u_6} →
    [inst : Field K] →
      [inst_1 : AddCommGroup V] →
        [inst_2 : Module K V] →
          {ι : Type u_9} →
            [DecidableEq ι] →
              [Finite ι] → (B : LinearMap.BilinForm K V) → B.Nondegenerate → Module.Basis ι K V → Module.Basis ι K V
-- Mathlib.MeasureTheory.Integral.TorusIntegral
torusMap_eq_center_iff : ∀ {n : ℕ} {c : Fin n → ℂ} {R θ : Fin n → ℝ}, torusMap c R θ = c ↔ R = 0
-- Mathlib.Algebra.Module.SpanRank
Ideal.lift_spanRank_map_le : ∀ {R : Type u} [inst : Semiring R] {T : Type v} [inst_1 : Semiring T] (f : R →+* T) (I : Ideal R),
  Cardinal.lift.{u, v} (Submodule.spanRank (Ideal.map f I)) ≤ Cardinal.lift.{v, u} (Submodule.spanRank I)
-- Mathlib.GroupTheory.FreeGroup.IsFreeGroup
FreeGroupBasis.ofRepr.sizeOf_spec : ∀ {ι : Type u_1} {G : Type u_2} [inst : Group G] [inst_1 : SizeOf ι] [inst_2 : SizeOf G] (repr : G ≃* FreeGroup ι),
  sizeOf { repr := repr } = 1 + sizeOf repr
-- Mathlib.LinearAlgebra.Dimension.Finite
exists_linearIndependent_of_le_finrank : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {n : ℕ},
  n ≤ Module.finrank R M → ∃ f, LinearIndependent R f
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.unop_op : ∀ {C : Type u} [inst : CategoryTheory.CategoryStruct.{v, u} C] (P : CategoryTheory.MorphismProperty C), P.op.unop = P
-- Lean.HeadIndex
Lean.HeadIndex.lam : Lean.HeadIndex
-- Mathlib.Lean.Meta.CongrTheorems
Lean.Meta.instFastSubsingleton : ∀ {p : Prop}, Lean.Meta.FastSubsingleton p
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.notMem_support_iff : ∀ {ι : Type u} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → Zero (β i)]
  [inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)] {f : Π₀ (i : ι), β i} {i : ι}, i ∉ f.support ↔ f i = 0
-- Mathlib.Data.List.Sort
List.sortedLE_map_toDual : ∀ {α : Type u_1} [inst : Preorder α] {l : List α}, (List.map (⇑OrderDual.toDual) l).SortedLE ↔ l.SortedGE
-- Mathlib.Probability.IdentDistrib
ProbabilityTheory.IdentDistrib.comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  [inst_2 : MeasurableSpace γ] [inst_3 : MeasurableSpace δ] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β}
  {f : α → γ} {g : β → γ} {u : γ → δ},
  ProbabilityTheory.IdentDistrib f g μ ν → Measurable u → ProbabilityTheory.IdentDistrib (u ∘ f) (u ∘ g) μ ν
-- Mathlib.CategoryTheory.Limits.Types.End
CategoryTheory.Limits.Types.coendRel_iff : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J]
  (F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J (Type (max w u)))) (j j' : J)
  (x : (F.obj (Opposite.op j)).obj j) (x' : (F.obj (Opposite.op j')).obj j'),
  CategoryTheory.Limits.Types.coendRel F ⟨j, x⟩ ⟨j', x'⟩ ↔
    ∃ f y,
      (CategoryTheory.ConcreteCategory.hom ((F.map f.op).app j)) y = x ∧
        (CategoryTheory.ConcreteCategory.hom ((F.obj (Opposite.op j')).map f)) y = x'
-- Mathlib.Algebra.Group.Hom.Defs
/-- The underlying function  -/
MulHom.toFun : {M : Type u_10} → {N : Type u_11} → [inst : Mul M] → [inst_1 : Mul N] → (M →ₙ* N) → M → N
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.pi_ne_zero : Real.pi ≠ 0
-- Mathlib.RingTheory.Smooth.Quotient
/-- For any surjection `f : M →ₗ[R] N`, with `N` a flat `R`-module,
we have `K ⊓ IM = IK` for any `I : Ideal R`.  -/
LinearMap.ker_inf_smul_top_eq_smul_of_flat : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} {N : Type u_3} [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup N]
  [inst_3 : Module R M] [inst_4 : Module R N] (I : Ideal R) (f : M →ₗ[R] N),
  Function.Surjective ⇑f → ∀ [Module.Flat R N], f.ker ⊓ I • ⊤ = I • f.ker
-- Mathlib.RingTheory.DedekindDomain.Instances
_private.Mathlib.RingTheory.DedekindDomain.Instances.0.termTₚ : Lean.ParserDescr
-- Mathlib.Analysis.SpecialFunctions.Complex.Log
Complex.log.eq_1 : ∀ (x : ℂ), Complex.log x = ↑(Real.log ‖x‖) + ↑x.arg * Complex.I
-- Mathlib.Data.EReal.Inv
EReal.instMulPosMono : MulPosMono EReal
-- Mathlib.Algebra.Group.Nat.Even
Nat.succ_mod_two_eq_zero_iff : ∀ {m : ℕ}, (m + 1) % 2 = 0 ↔ m % 2 = 1
-- Mathlib.Algebra.GroupWithZero.Pi
Pi.mulZeroOneClass : {ι : Type u_1} → {α : ι → Type u_2} → [(i : ι) → MulZeroOneClass (α i)] → MulZeroOneClass ((i : ι) → α i)
-- Mathlib.MeasureTheory.Measure.GiryMonad
MeasureTheory.Measure.measurable_coe : ∀ {α : Type u_1} {mα : MeasurableSpace α} {s : Set α}, MeasurableSet s → Measurable fun μ => μ s
-- Mathlib.Order.Defs.Unbundled
/-- `IsTotal X r` means that the binary relation `r` on `X` is total, that is, that for any
`x y : X` we have `r x y` or `r y x`.  -/
IsTotal : (α : Sort u_1) → (α → α → Prop) → Prop
-- Mathlib.CategoryTheory.Simple
CategoryTheory.simple_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {D : Type u_1} [inst_2 : CategoryTheory.Category.{v_1, u_1} D] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  (F : CategoryTheory.Functor C D) [F.IsEquivalence] (X : C) [CategoryTheory.Simple X], CategoryTheory.Simple (F.obj X)
-- Mathlib.MeasureTheory.Measure.AEMeasurable
/-- Let `f : α → β` be a null measurable function
such that a.e. all values of `f` belong to a set `t`
such that the restriction of the `σ`-algebra in the codomain to `t` is countably generated,
then `f` is a.e.-measurable.  -/
MeasureTheory.NullMeasurable.aemeasurable_of_aerange : ∀ {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [inst : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {f : α → β} {t : Set β} [MeasurableSpace.CountablyGenerated ↑t],
  MeasureTheory.NullMeasurable f μ → (∀ᵐ (x : α) ∂μ, f x ∈ t) → AEMeasurable f μ
-- Mathlib.Topology.Category.Stonean.EffectiveEpi
Stonean.instReflectsEffectiveEpisCompHausToCompHaus : Stonean.toCompHaus.ReflectsEffectiveEpis
-- Mathlib.RingTheory.Spectrum.Prime.Module
Module.isClosed_support : ∀ {R : Type u_1} {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [Module.Finite R M],
  IsClosed (Module.support R M)
-- Mathlib.Logic.Equiv.Defs
Equiv.eq_comp_symm : ∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (e : α ≃ β) (f : β → γ) (g : α → γ), f = g ∘ ⇑e.symm ↔ f ∘ ⇑e = g
-- Mathlib.Analysis.Convex.SpecificFunctions.Basic
/-- `Real.exp` is strictly convex on the whole real line.  -/
strictConvexOn_exp : StrictConvexOn ℝ Set.univ Real.exp
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.coe_one : ⇑1 = id
-- Mathlib.Analysis.Calculus.FDeriv.Prod
DifferentiableOn.snd : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {s : Set E} {f₂ : E → F × G},
  DifferentiableOn 𝕜 f₂ s → DifferentiableOn 𝕜 (fun x => (f₂ x).2) s
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.aeval_X_left_apply : ∀ {R : Type u} [inst : CommSemiring R] (p : Polynomial R), (Polynomial.aeval Polynomial.X) p = p
-- Mathlib.Combinatorics.KatonaCircle
Numbering.mem_prefixed : ∀ {X : Type u_1} [inst : Fintype X] {f : Numbering X} {s : Finset X} [inst_1 : DecidableEq X],
  f ∈ Numbering.prefixed s ↔ f.IsPrefix s
-- Mathlib.Algebra.Module.Submodule.Ker
LinearMap.ker_smul' : ∀ {K : Type u_4} {V : Type u_9} {V₂ : Type u_10} [inst : Semifield K] [inst_1 : AddCommMonoid V] [inst_2 : Module K V]
  [inst_3 : AddCommMonoid V₂] [inst_4 : Module K V₂] (f : V →ₗ[K] V₂) (a : K), (a • f).ker = ⨅ (_ : a ≠ 0), f.ker
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F : C ⥤ Dᵒᵖ` reflects limits of shape `Jᵒᵖ`, then `F.leftOp : Cᵒᵖ ⥤ D` reflects colimits
of shape `J`.  -/
CategoryTheory.Limits.reflectsColimitsOfShape_leftOp : ∀ {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 C Dᵒᵖ)
  [CategoryTheory.Limits.ReflectsLimitsOfShape Jᵒᵖ F], CategoryTheory.Limits.ReflectsColimitsOfShape J F.leftOp
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.HasImage.mk' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y},
  Nonempty (CategoryTheory.Limits.ImageFactorisation f) → CategoryTheory.Limits.HasImage f
-- Mathlib.Order.Filter.Extr
IsMaxFilter.sub : ∀ {α : Type u} {β : Type v} [inst : AddCommGroup β] [inst_1 : PartialOrder β] [IsOrderedAddMonoid β] {f g : α → β}
  {a : α} {l : Filter α}, IsMaxFilter f l a → IsMinFilter g l a → IsMaxFilter (fun x => f x - g x) l a
-- Mathlib.ModelTheory.ElementaryMaps
/-- An elementary embedding is also a first-order homomorphism.  -/
FirstOrder.Language.ElementaryEmbedding.toHom : {L : FirstOrder.Language} →
  {M : Type u_1} →
    {N : Type u_2} → [inst : L.Structure M] → [inst_1 : L.Structure N] → L.ElementaryEmbedding M N → L.Hom M N
-- Mathlib.CategoryTheory.Abelian.Projective.Dimension
CategoryTheory.Abelian.Ext.eq_zero_of_hasProjectiveDimensionLT : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] {X Y : C} {i : ℕ} (e : CategoryTheory.Abelian.Ext X Y i) (n : ℕ)
  [CategoryTheory.HasProjectiveDimensionLT X n], n ≤ i → e = 0
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
/-- Real powers of operators, based on the unital continuous functional calculus.  -/
CFC.rpow : {A : Type u_1} →
  [inst : PartialOrder A] →
    [inst_1 : Ring A] →
      [inst_2 : StarRing A] →
        [inst_3 : TopologicalSpace A] →
          [StarOrderedRing A] →
            [inst_5 : Algebra ℝ A] →
              [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] → [NonnegSpectrumClass ℝ A] → A → ℝ → A
-- Mathlib.Order.CompleteSublattice
/-- To check that a subset is a complete sublattice, one does not need to check that it is closed
under binary `Sup` since this follows from the stronger `sSup` condition. Likewise for infima.  -/
CompleteSublattice.mk' : {α : Type u_1} →
  [inst : CompleteLattice α] →
    (carrier : Set α) →
      (∀ ⦃s : Set α⦄, s ⊆ carrier → sSup s ∈ carrier) →
        (∀ ⦃s : Set α⦄, s ⊆ carrier → sInf s ∈ carrier) → CompleteSublattice α
-- Mathlib.AlgebraicGeometry.Birational.Birational
/-- Restrict the target of a partial isomorphism to a smaller dense open.  -/
AlgebraicGeometry.Scheme.PartialIso.restrictTarget : {X Y : AlgebraicGeometry.Scheme} → (f : X.PartialIso Y) → (U : Y.Opens) → Dense ↑U → U ≤ f.target → X.PartialIso Y
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Equiv.inter_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ m₃ : Std.DHashMap.Internal.Raw₀ α β}
  [EquivBEq α] [LawfulHashable α],
  (↑m₁).WF → (↑m₂).WF → (↑m₃).WF → (↑m₂).Equiv ↑m₃ → (↑(m₁.inter m₂)).Equiv ↑(m₁.inter m₃)
-- Mathlib.MeasureTheory.Measure.Restrict
/-- If a quasi-measure-preserving map `f` maps a set `s` to a set `t`,
then it is quasi-measure-preserving with respect to the restrictions of the measures.  -/
MeasureTheory.Measure.QuasiMeasurePreserving.restrict : ∀ {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [inst : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {s : Set α} {ν : MeasureTheory.Measure β} {f : α → β},
  MeasureTheory.Measure.QuasiMeasurePreserving f μ ν →
    ∀ {t : Set β}, Set.MapsTo f s t → MeasureTheory.Measure.QuasiMeasurePreserving f (μ.restrict s) (ν.restrict t)
-- Mathlib.Topology.Instances.TrivSqZeroExt
TrivSqZeroExt.instIsTopologicalRingOfIsTopologicalAddGroupOfContinuousSMulMulOpposite : ∀ {R : Type u_3} {M : Type u_4} [inst : TopologicalSpace R] [inst_1 : TopologicalSpace M] [inst_2 : Ring R]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : Module Rᵐᵒᵖ M] [IsTopologicalRing R]
  [IsTopologicalAddGroup M] [ContinuousSMul R M] [ContinuousSMul Rᵐᵒᵖ M], IsTopologicalRing (TrivSqZeroExt R M)
-- Std.Sync.Broadcast
Std.Broadcast.Receiver.instAsyncStreamOptionOfInhabited : {α : Type} → [Inhabited α] → Std.Async.IO.AsyncStream (Std.Broadcast.Receiver α) (Option α)
-- Mathlib.Tactic.Linter.Header
/-- `isInLibraryRoot modName` returns `true` if `<root>.lean` imports the file `modName`, where
`<root>` is the top-level component of `modName`. For example, for `Mathlib.Foo.Bar` this checks
`Mathlib.lean`; for `Cslib.Foo.Bar` this checks `Cslib.lean`.
This is used by the `Header` linter as a heuristic of whether it should inspect the file or not,
so that the linter works in any project whose library root follows the standard Lean convention
of being named after the top-level module.
 -/
_private.Mathlib.Tactic.Linter.Header.0.Mathlib.Linter.isInLibraryRoot : Lean.Name → IO Bool
-- Init.Data.UInt.Lemmas
UInt64.lt_of_lt_of_le : ∀ {a b c : UInt64}, a < b → b ≤ c → a < c
-- Lean.CoreM
Lean.Elab.inServer : Lean.Option Bool
-- Init.Data.Array.Lemmas
Array.any_reverse : ∀ {α : Type u_1} {f : α → Bool} {xs : Array α}, xs.reverse.any f = xs.any f
-- Mathlib.GroupTheory.Complement
Subgroup.IsComplement.equiv_mul_left : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} {T : Set G} (hHT : Subgroup.IsComplement (↑H) T) (h : ↥H) (g : G),
  hHT.equiv (↑h * g) = (h * (hHT.equiv g).1, (hHT.equiv g).2)