mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.ShortComplex.Exact
/-- A short complex equipped with a splitting is exact.  -/
CategoryTheory.ShortComplex.Splitting.exact : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S : CategoryTheory.ShortComplex C} [CategoryTheory.Limits.HasZeroObject C] (s : S.Splitting), S.Exact
-- Mathlib.CategoryTheory.Monad.EquivMon
/-- Passing from `Mon (C ⥤ C)` to `Monad C` is functorial.  -/
CategoryTheory.Monad.monToMonad : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.Functor (CategoryTheory.Mon (CategoryTheory.Functor C C)) (CategoryTheory.Monad C)
-- Mathlib.Tactic.Linter.DirectoryDependency
/-- Collect all prefixes of names in `ns` into a single `NameSet`.  -/
_private.Mathlib.Tactic.Linter.DirectoryDependency.0.Lean.Name.collectPrefixes : Array Lean.Name → Lean.NameSet
-- Mathlib.Order.Hom.Lattice
InfHom.instOrderBot : {α : Type u_2} → {β : Type u_3} → [inst : Min α] → [inst_1 : SemilatticeInf β] → [OrderBot β] → OrderBot (InfHom α β)
-- Init.Data.List.Erase
List.erase_replicate_ne : ∀ {α : Type u_1} [inst : BEq α] {n : ℕ} [LawfulBEq α] {a b : α},
  (!b == a) = true → (List.replicate n a).erase b = List.replicate n a
-- Mathlib.CategoryTheory.Limits.Types.Filtered
CategoryTheory.Limits.Types.FilteredColimit.rel_eq_eqvGen_colimitTypeRel : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J (Type u))
  [CategoryTheory.IsFilteredOrEmpty J],
  CategoryTheory.Limits.Types.FilteredColimit.Rel F = Relation.EqvGen F.ColimitTypeRel
-- Mathlib.LinearAlgebra.ExteriorAlgebra.Basis
ExteriorAlgebra.basis_apply_powersetCard : ∀ {R : Type u_1} {M : Type u_2} {m : ℕ} {I : Type u_3} [inst : LinearOrder I] [inst_1 : CommRing R]
  [inst_2 : AddCommGroup M] [inst_3 : Module R M] (b : Module.Basis I R M) (s : ↑(Set.powersetCard I m)),
  b.ExteriorAlgebra ↑s = ExteriorAlgebra.ιMulti_family R m (⇑b) s
-- Lean.Util.HasConstCache
/-- Return true iff `e` contains the constant `declName`.
Remark: the results for visited expressions are stored in the state cache.  -/
Lean.HasConstCache.contains : {declNames : Array Lean.Name} → Lean.Expr → StateM (Lean.HasConstCache declNames) Bool
-- Mathlib.Combinatorics.Enumerative.Composition
Composition.mk.sizeOf_spec : ∀ {n : ℕ} (blocks : List ℕ) (blocks_pos : ∀ {i : ℕ}, i ∈ blocks → 0 < i) (blocks_sum : blocks.sum = n),
  sizeOf { blocks := blocks, blocks_pos := blocks_pos, blocks_sum := blocks_sum } =
    1 + sizeOf blocks + sizeOf blocks_sum
-- Mathlib.Combinatorics.HalesJewett
Combinatorics.Line.ColorFocused.mk.injEq : ∀ {α : Type u_5} {ι : Type u_6} {κ : Type u_7} {C : (ι → Option α) → κ}
  (lines : Multiset (Combinatorics.Line.AlmostMono C)) (focus : ι → Option α)
  (is_focused : ∀ p ∈ lines, ↑p.line none = focus)
  (distinct_colors : (Multiset.map Combinatorics.Line.AlmostMono.color lines).Nodup)
  (lines_1 : Multiset (Combinatorics.Line.AlmostMono C)) (focus_1 : ι → Option α)
  (is_focused_1 : ∀ p ∈ lines_1, ↑p.line none = focus_1)
  (distinct_colors_1 : (Multiset.map Combinatorics.Line.AlmostMono.color lines_1).Nodup),
  ({ lines := lines, focus := focus, is_focused := is_focused, distinct_colors := distinct_colors } =
      { lines := lines_1, focus := focus_1, is_focused := is_focused_1, distinct_colors := distinct_colors_1 }) =
    (lines = lines_1 ∧ focus = focus_1)
-- Mathlib.Analysis.Meromorphic.Basic
/-- Eta-expanded form of `Meromorphic.smul` -/
Meromorphic.fun_smul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {R : Type u_4} [inst_3 : NormedRing R] [inst_4 : Module R E] [IsBoundedSMul R E]
  {g : 𝕜 → E} [inst_6 : NormedAlgebra 𝕜 R] [IsScalarTower 𝕜 R E] {f : 𝕜 → R},
  Meromorphic f → Meromorphic g → Meromorphic fun i => f i • g i
-- Mathlib.RingTheory.MvPowerSeries.Expand
MvPowerSeries.expand_X : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommRing R] (p : ℕ) (hp : p ≠ 0) (i : σ),
  (MvPowerSeries.expand p hp) (MvPowerSeries.X i) = MvPowerSeries.X i ^ p
-- Mathlib.Algebra.Homology.ShortComplex.Limits
/-- `colimitCocone F` becomes colimit after the application of `π₁ : ShortComplex C ⥤ C`.  -/
CategoryTheory.ShortComplex.isColimitπ₁MapCoconeColimitCocone : {J : Type u_1} →
  {C : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} J] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} C] →
        [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
          (F : CategoryTheory.Functor J (CategoryTheory.ShortComplex C)) →
            [inst_3 : CategoryTheory.Limits.HasColimit (F.comp CategoryTheory.ShortComplex.π₁)] →
              [inst_4 : CategoryTheory.Limits.HasColimit (F.comp CategoryTheory.ShortComplex.π₂)] →
                [inst_5 : CategoryTheory.Limits.HasColimit (F.comp CategoryTheory.ShortComplex.π₃)] →
                  CategoryTheory.Limits.IsColimit
                    (CategoryTheory.ShortComplex.π₁.mapCocone (CategoryTheory.ShortComplex.colimitCocone F))
-- Mathlib.Algebra.MonoidAlgebra.Defs
/-- A product monoid algebra is a nested monoid algebra.  -/
MonoidAlgebra.curryAddEquiv : {R : Type u_1} →
  {M : Type u_4} →
    {N : Type u_5} →
      [inst : Semiring R] →
        [inst_1 : Monoid M] → [inst_2 : Monoid N] → MonoidAlgebra R (M × N) ≃+ MonoidAlgebra (MonoidAlgebra R N) M
-- Mathlib.RingTheory.PicardGroup
_private.Mathlib.RingTheory.PicardGroup.0.CommRing.Pic.equivShrinkLinearEquiv : (R : Type u) →
  [inst : CommSemiring R] →
    (M : (CategoryTheory.Skeleton (SemimoduleCat R))ˣ) →
      (id ((equivShrink (CategoryTheory.Skeleton (SemimoduleCat R))ˣ) M)).AsModule ≃ₗ[R] ↑(Quotient.out ↑M)
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
NumberField.InfinitePlace.mult_ne_zero : ∀ {K : Type u_1} [inst : Field K] {w : NumberField.InfinitePlace K}, w.mult ≠ 0
-- Mathlib.Topology.MetricSpace.Algebra
/-- Eta-expanded form of `TendstoLocallyUniformly.smul₀_of_isBoundedUnder` -/
TendstoLocallyUniformly.fun_smul₀_of_isBoundedUnder : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] [inst_2 : Zero α]
  [inst_3 : Zero β] [inst_4 : SMul α β] [IsBoundedSMul α β] {X : Type u_3} {ι : Type u_4} [inst_6 : TopologicalSpace X]
  {F : ι → X → α} {G : ι → X → β} {f : X → α} {g : X → β} {l : Filter ι},
  TendstoLocallyUniformly F f l →
    TendstoLocallyUniformly G g l →
      (∀ (x : X), Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) (nhds x) fun y => dist (f y) 0) →
        (∀ (x : X), Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) (nhds x) fun y => dist (g y) 0) →
          TendstoLocallyUniformly (fun i i_1 => F i i_1 • G i i_1) (fun i => f i • g i) l
-- Mathlib.RepresentationTheory.Intertwining
Representation.Equiv.mk_symm : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Semiring A] [inst_1 : Monoid G]
  [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid W] [inst_4 : Module A V] [inst_5 : Module A W]
  {ρ : Representation A G V} {σ : Representation A G W} {e : V ≃ₗ[A] W} (he : ∀ (g : G), ↑e ∘ₗ ρ g = σ g ∘ₗ ↑e),
  (Representation.Equiv.mk e he).symm = Representation.Equiv.mk e.symm ⋯
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
MeasurableSpace.GenerateMeasurable.below.basic : ∀ {α : Type u_1} {s : Set (Set α)} {motive : (a : Set α) → MeasurableSpace.GenerateMeasurable s a → Prop} (u : Set α)
  (a : u ∈ s), MeasurableSpace.GenerateMeasurable.below ⋯
-- Mathlib.Order.Interval.Set.Image
Set.image_subtype_val_Icc_Iio : ∀ {α : Type u_1} [inst : Preorder α] {a b : α} (c : ↑(Set.Icc a b)), Subtype.val '' Set.Iio c = Set.Ico a ↑c
-- Mathlib.Analysis.Normed.Group.Defs
NormedGroup.toNorm : {E : Type u_8} → [self : NormedGroup E] → Norm E
-- Mathlib.GroupTheory.Coset.Card
QuotientAddGroup.fintypeQuotientRightRel : {α : Type u_1} →
  [inst : AddGroup α] → {s : AddSubgroup α} → [Fintype (α ⧸ s)] → Fintype (Quotient (QuotientAddGroup.rightRel s))
-- Lean.Elab.Tactic.Omega.Core
/-- Add a constraint into the problem,
combining it with any existing constraints for the same coefficients.
 -/
Lean.Elab.Tactic.Omega.Problem.addConstraint : Lean.Elab.Tactic.Omega.Problem → Lean.Elab.Tactic.Omega.Fact → Lean.Elab.Tactic.Omega.Problem
-- Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit
CochainComplex.homOfDegreewiseSplit_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (S : CategoryTheory.ShortComplex (CochainComplex C ℤ))
  (σ : (n : ℤ) → (S.map (HomologicalComplex.eval C (ComplexShape.up ℤ) n)).Splitting) (n : ℤ),
  (CochainComplex.homOfDegreewiseSplit S σ).f n = (↑(CochainComplex.cocycleOfDegreewiseSplit S σ)).v n (n + 1) ⋯
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
NumberField.mixedEmbedding.fundamentalCone.injective_expMap : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  Function.Injective ↑NumberField.mixedEmbedding.fundamentalCone.expMap
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
MeasureTheory.condExp_def : ∀ {α : Type u_5} {E : Type u_6} (m : MeasurableSpace α) {m₀ : MeasurableSpace α} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] (μ : MeasureTheory.Measure α) (f : α → E),
  μ[f | m] =
    if hm : m ≤ m₀ then
      if h : MeasureTheory.SigmaFinite (μ.trim hm) ∧ MeasureTheory.Integrable f μ then
        if MeasureTheory.StronglyMeasurable f then f
        else
          have this := ⋯;
          MeasureTheory.AEStronglyMeasurable.mk ↑↑(MeasureTheory.condExpL1 hm μ f) ⋯
      else 0
    else 0
-- Mathlib.RingTheory.Valuation.Quotient
/-- The extension of valuation `v` on `R` to valuation on `R / J` if `J ⊆ supp v`.  -/
AddValuation.onQuot : {R : Type u_1} →
  {Γ₀ : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : LinearOrderedAddCommMonoidWithTop Γ₀] →
        (v : AddValuation R Γ₀) → {J : Ideal R} → J ≤ v.supp → AddValuation (R ⧸ J) Γ₀
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.homEquiv_naturality_left_square_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) {X' X : C} {Y Y' : D} (f : X' ⟶ X)
  (g : F.obj X ⟶ Y') (h : F.obj X' ⟶ Y) (k : Y ⟶ Y'),
  CategoryTheory.CategoryStruct.comp (F.map f) g = CategoryTheory.CategoryStruct.comp h k →
    ∀ {Z : C} (h_1 : G.obj Y' ⟶ Z),
      CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp ((adj.homEquiv X Y') g) h_1) =
        CategoryTheory.CategoryStruct.comp ((adj.homEquiv X' Y) h) (CategoryTheory.CategoryStruct.comp (G.map k) h_1)
-- Mathlib.Algebra.Group.Equiv.Defs
/-- The identity equivalence between the monoid of endomorphisms `Monoid.End M` and the type
`M →* M` of monoid homomorphisms from `M` to itself. `Monoid.End M` is definitionally (but not
reducibly) equal to `M →* M`.  -/
Monoid.End.equiv : (M : Type u_9) → [inst : MulOne M] → Monoid.End M ≃ (M →* M)
-- Lean.Meta.Tactic.Grind.Parser
Lean.Parser.Command.GrindCnstr.depthLt.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.CategoryTheory.Grothendieck
CategoryTheory.Grothendieck.pre_map_fiber : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} D]
  (F : CategoryTheory.Functor C CategoryTheory.Cat) (G : CategoryTheory.Functor D C)
  {X Y : CategoryTheory.Grothendieck (G.comp F)} (f : X ⟶ Y),
  ((CategoryTheory.Grothendieck.pre F G).map f).fiber = f.fiber
-- Mathlib.Topology.Category.TopCat.Opens
TopologicalSpace.Opens.inclusion'_hom_apply : ∀ {X : TopCat} (U : TopologicalSpace.Opens ↑X), ⇑(TopCat.Hom.hom U.inclusion') = Subtype.val
-- Mathlib.GroupTheory.MonoidLocalization.Maps
Localization.mulEquivOfQuotient_symm_mk : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N]
  {f : S.LocalizationMap N} (x : M) (y : ↥S), (Localization.mulEquivOfQuotient f).symm (f.mk' x y) = Localization.mk x y
-- Init.Data.UInt.Lemmas
USize.toBitVec_toUInt8 : ∀ (n : USize), n.toUInt8.toBitVec = BitVec.setWidth 8 n.toBitVec
-- Mathlib.Data.Set.Function
/-- If functions `f'` and `f` are inverse on `s` and `t`, `f` maps `s` into `t`, and `f'` maps `t`
into `s`, then `f` is a bijection between `s` and `t`. The `mapsTo` arguments can be deduced from
`surjOn` statements using `LeftInvOn.mapsTo` and `RightInvOn.mapsTo`.  -/
Set.InvOn.bijOn : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β} {f' : β → α},
  Set.InvOn f' f s t → Set.MapsTo f s t → Set.MapsTo f' t s → Set.BijOn f s t
-- Mathlib.Algebra.Polynomial.CoeffList
Polynomial.length_coeffList_eq_ite : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : DecidableEq R] (P : Polynomial R),
  P.coeffList.length = if P = 0 then 0 else P.natDegree + 1
-- Mathlib.Analysis.Convex.Function
concaveOn_iff_convex_hypograph : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommMonoid β] [inst_4 : PartialOrder β] [IsOrderedAddMonoid β] [inst_6 : SMul 𝕜 E] [inst_7 : Module 𝕜 β]
  [PosSMulMono 𝕜 β] {s : Set E} {f : E → β}, ConcaveOn 𝕜 s f ↔ Convex 𝕜 {p | p.1 ∈ s ∧ p.2 ≤ f p.1}
-- Mathlib.Algebra.Group.Finsupp
/-- A finitely supported function can be built by adding up `single a b` for decreasing `a`.

The lemma `induction_on_min₂` swaps the argument order in the sum.  -/
Finsupp.induction_on_min : ∀ {ι : Type u_1} {M : Type u_3} [inst : AddZeroClass M] [inst_1 : LinearOrder ι] {motive : (ι →₀ M) → Prop}
  (f : ι →₀ M),
  motive 0 →
    (∀ (a : ι) (b : M) (f : ι →₀ M), (∀ c ∈ f.support, a < c) → b ≠ 0 → motive f → motive ((fun₀ | a => b) + f)) →
      motive f
-- Mathlib.MeasureTheory.VectorMeasure.Integral
/-- `f : X → E` is said to be integrable with respect to `μ` and `B` on `s` if it is integrable with
respect to the vector measure `μ.restrict s`. When `s` is measurable, this is equivalent to
integrability with respect to `(μ.transpose B).variation.restrict s`.  -/
MeasureTheory.VectorMeasure.IntegrableOn : {X : Type u_2} →
  {E : Type u_4} →
    {F : Type u_5} →
      {mX : MeasurableSpace X} →
        [NormedAddCommGroup E] →
          [inst : NormedAddCommGroup F] → MeasureTheory.VectorMeasure X F → (X → E) → Set X → Prop
-- Mathlib.Data.Ordmap.Ordnode
/-- Convert to an `BinaryTree`, discarding the cached size information.  -/
Ordnode.toBinaryTree : {α : Type u_1} → Ordnode α → BinaryTree α
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Antitone.mul_const' : ∀ {α : Type u_1} {β : Type u_2} [inst : Mul α] [inst_1 : Preorder α] [inst_2 : Preorder β] {f : β → α} [MulRightMono α],
  Antitone f → ∀ (a : α), Antitone fun x => f x * a
-- Mathlib.Order.SuccPred.Basic
Order.Ioi_pred : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : PredOrder α] [NoMinOrder α] (a : α),
  Set.Ioi (Order.pred a) = Set.Ici a
-- Mathlib.CategoryTheory.Limits.Creates
CategoryTheory.LiftableCocone.mk : {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] →
            {K : CategoryTheory.Functor J C} →
              {F : CategoryTheory.Functor C D} →
                {c : CategoryTheory.Limits.Cocone (K.comp F)} →
                  (liftedCocone : CategoryTheory.Limits.Cocone K) →
                    (F.mapCocone liftedCocone ≅ c) → CategoryTheory.LiftableCocone K F c
-- Mathlib.Algebra.GroupWithZero.Basic
/-- **Alias** of the forward direction of `subsingleton_iff_zero_eq_one`.

---

In a monoid with zero, zero equals one if and only if all elements of that semiring
are equal.  -/
subsingleton_of_zero_eq_one : ∀ {M₀ : Type u_1} [inst : MulZeroOneClass M₀], 0 = 1 → Subsingleton M₀
-- Mathlib.CategoryTheory.Comma.Presheaf.Colimit
_private.Mathlib.CategoryTheory.Comma.Presheaf.Colimit.0.CategoryTheory.termE : Lean.ParserDescr
-- Mathlib.Computability.AkraBazzi.AkraBazzi
AkraBazziRecurrence.isBigO_apply_r_sub_b : ∀ {α : Type u_1} [inst : Fintype α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ} [inst_1 : Nonempty α]
  (R : AkraBazziRecurrence T g a b r) (q : ℝ → ℝ),
  DifferentiableOn ℝ q (Set.Ioi 1) →
    (AkraBazziRecurrence.GrowsPolynomially fun x => ‖deriv q x‖) →
      ∀ (i : α), (fun n => q ↑(r i n) - q (b i * ↑n)) =O[Filter.atTop] fun n => deriv q ↑n * (↑(r i n) - b i * ↑n)
-- Mathlib.Topology.VectorBundle.Basic
VectorBundleCore.fiberBundle : {R : Type u_1} →
  {B : Type u_2} →
    {F : Type u_3} →
      [inst : NontriviallyNormedField R] →
        [inst_1 : NormedAddCommGroup F] →
          [inst_2 : NormedSpace R F] →
            [inst_3 : TopologicalSpace B] → {ι : Type u_5} → (Z : VectorBundleCore R B F ι) → FiberBundle F Z.Fiber
-- Mathlib.Tactic.TermCongr
/-- (Internal for `congr(...)`)
Elaborates to an expression satisfying `cHole?` that equals the LHS or RHS of `h`,
if the LHS or RHS is available after elaborating `h`. Uses the expected type as a hint.  -/
Mathlib.Tactic.TermCongr.cHoleExpand : Lean.ParserDescr
-- Std.Data.DTreeMap.Internal.Balancing
/-- Precondition for `balanceL`: at most one element was added to left subtree.  -/
Std.DTreeMap.Internal.Impl.BalanceLPrecond : ℕ → ℕ → Prop
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.measurePreserving_sub_right : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : AddGroup G] [MeasurableAdd G] (μ : MeasureTheory.Measure G)
  [μ.IsAddRightInvariant] (g : G), MeasureTheory.MeasurePreserving (fun x => x - g) μ μ
-- Mathlib.Algebra.Polynomial.Reverse
Polynomial.reverse_trailingCoeff : ∀ {R : Type u_1} [inst : Semiring R] (f : Polynomial R), f.reverse.trailingCoeff = f.leadingCoeff
-- Mathlib.GroupTheory.Coset.Defs
/-- Right cosets are in bijection with left cosets.  -/
QuotientGroup.quotientRightRelEquivQuotientLeftRel : {α : Type u_1} → [inst : Group α] → (s : Subgroup α) → Quotient (QuotientGroup.rightRel s) ≃ α ⧸ s
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
ContinuousLinearMapWOT.comp_apply : ∀ {𝕜₁ : Type u_5} {𝕜₂ : Type u_6} {𝕜₃ : Type u_7} {E : Type u_9} {F : Type u_10} {G : Type u_11} [inst : NormedField 𝕜₁]
  [inst_1 : NormedField 𝕜₂] [inst_2 : NormedField 𝕜₃] {σ₁₂ : 𝕜₁ →+* 𝕜₂} {σ₁₃ : 𝕜₁ →+* 𝕜₃} {σ₂₃ : 𝕜₂ →+* 𝕜₃}
  [inst_3 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [inst_4 : AddCommGroup E] [inst_5 : TopologicalSpace E]
  [inst_6 : Module 𝕜₁ E] [inst_7 : AddCommGroup F] [inst_8 : TopologicalSpace F] [inst_9 : Module 𝕜₂ F]
  [inst_10 : AddCommGroup G] [inst_11 : TopologicalSpace G] [inst_12 : Module 𝕜₃ G] (g : F →SWOT[σ₂₃] G)
  (f : E →SWOT[σ₁₂] F) (x : E), (g.comp f) x = g (f x)
-- Mathlib.GroupTheory.PushoutI
Monoid.PushoutI.of_apply_eq_base : ∀ {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [inst : (i : ι) → Monoid (G i)] [inst_1 : Monoid H]
  (φ : (i : ι) → H →* G i) (i : ι) (x : H), (Monoid.PushoutI.of i) ((φ i) x) = (Monoid.PushoutI.base φ) x
-- Mathlib.CategoryTheory.Limits.Types.Coequalizers
/-- If `π : Y ⟶ Z` is a coequalizer for `(f, g)`, and `U ⊆ Y` such that `f ⁻¹' U = g ⁻¹' U`,
then `π ⁻¹' π '' U = U`.
 -/
CategoryTheory.Limits.Types.coequalizer_preimage_image_eq_of_preimage_eq : ∀ {X Y Z : Type u} (f g : X ⟶ Y) (π : Y ⟶ Z)
  (e : CategoryTheory.CategoryStruct.comp f π = CategoryTheory.CategoryStruct.comp g π)
  (h : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofork.ofπ π e)) (U : Set Y),
  ⇑(CategoryTheory.ConcreteCategory.hom f) ⁻¹' U = ⇑(CategoryTheory.ConcreteCategory.hom g) ⁻¹' U →
    ⇑(CategoryTheory.ConcreteCategory.hom π) ⁻¹' ⇑(CategoryTheory.ConcreteCategory.hom π) '' U = U
-- Mathlib.MeasureTheory.Integral.Gamma
integral_exp_neg_rpow : ∀ {p : ℝ}, 0 < p → ∫ (x : ℝ) in Set.Ioi 0, Real.exp (-x ^ p) = Real.Gamma (1 / p + 1)
-- Mathlib.AlgebraicGeometry.Modules.Tilde
_private.Mathlib.AlgebraicGeometry.Modules.Tilde.0.AlgebraicGeometry.QuasicoherentTilde.isLocalizing_iff_aux : ∀ {R : CommRingCat} (M : (AlgebraicGeometry.Spec R).Modules),
  AlgebraicGeometry.IsLocalizing (AlgebraicGeometry.modulesSpecToSheaf.obj M) ↔
    AlgebraicGeometry.QuasicoherentTilde.Aux✝ M ⊤
-- Lean.Meta.Canonicalizer
/-- "Canonicalize" the given expression.
 -/
Lean.Meta.Canonicalizer.canon : Lean.Expr → Lean.Meta.CanonM Lean.Expr
-- Mathlib.CategoryTheory.Sites.Adjunction
CategoryTheory.Sheaf.preservesSheafification_of_adjunction : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] {E : Type u_1} [inst_2 : CategoryTheory.Category.{v_1, u_1} E]
  {F : CategoryTheory.Functor D E} {G : CategoryTheory.Functor E D} (adj : G ⊣ F), J.PreservesSheafification G
-- Mathlib.Analysis.InnerProductSpace.TwoDim
Orientation.inner_rightAngleRotationAux₁_left : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : Fact (Module.finrank ℝ E = 2)]
  (o : Orientation ℝ E (Fin 2)) (x y : E), inner ℝ (o.rightAngleRotationAux₁ x) y = (o.areaForm x) y
-- Mathlib.RingTheory.MvPowerSeries.Inverse
MvPowerSeries.X_inv : ∀ {σ : Type u_1} {k : Type u_3} [inst : Field k] (s : σ), (MvPowerSeries.X s)⁻¹ = 0
-- Mathlib.Combinatorics.SimpleGraph.Copy
SimpleGraph.not_free : ∀ {α : Type u_4} {β : Type u_5} {A : SimpleGraph α} {B : SimpleGraph β}, ¬A.Free B ↔ A.IsContained B
-- Mathlib.Algebra.Category.Ring.Instances
CommRingCat.isLocalHom_comp : ∀ {R S T : CommRingCat} (f : R ⟶ S) (g : S ⟶ T) [IsLocalHom (CommRingCat.Hom.hom g)]
  [IsLocalHom (CommRingCat.Hom.hom f)], IsLocalHom (CommRingCat.Hom.hom (CategoryTheory.CategoryStruct.comp f g))
-- Mathlib.Analysis.Subadditive
/-- Fekete's lemma: a subadditive sequence which is bounded below converges.  -/
Subadditive.tendsto_lim : ∀ {u : ℕ → ℝ} (h : Subadditive u),
  BddBelow (Set.range fun n => u n / ↑n) → Filter.Tendsto (fun n => u n / ↑n) Filter.atTop (nhds h.lim)
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
/-- Build a new pseudometric space from an old one where the bundled bornology structure is provably
(but typically non-definitionaly) equal to some given bornology structure.
See Note [forgetful inheritance].
See Note [reducible non-instances].
 -/
PseudoMetricSpace.replaceBornology : {α : Type u_3} →
  [B : Bornology α] →
    (m : PseudoMetricSpace α) → (∀ (s : Set α), Bornology.IsBounded s ↔ Bornology.IsBounded s) → PseudoMetricSpace α
-- Mathlib.Data.Set.Functor
Set.instCommApplicative : CommApplicative Set
-- Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
WeierstrassCurve.VariableChange.map_u : ∀ {R : Type u} [inst : CommRing R] (C : WeierstrassCurve.VariableChange R) {A : Type v} [inst_1 : CommRing A]
  (φ : R →+* A), (C.map φ).u = (Units.map ↑φ) C.u
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.degree_smul_of_isRightRegular_leadingCoeff : ∀ {R : Type u} {a : R} [inst : Semiring R] {p : Polynomial R},
  a ≠ 0 → IsRightRegular p.leadingCoeff → (a • p).degree = p.degree
-- Mathlib.Algebra.Category.Ring.Basic
/-- The underlying type.  -/
CommSemiRingCat.carrier : CommSemiRingCat → Type u
-- Mathlib.RingTheory.IntegralClosure.Algebra.Basic
IsIntegral.neg : ∀ {R : Type u_1} {B : Type u_3} [inst : CommRing R] [inst_1 : Ring B] [inst_2 : Algebra R B] {x : B},
  IsIntegral R x → IsIntegral R (-x)
-- Mathlib.Geometry.Euclidean.Angle.Sphere
/-- Oriented angle version of "angles in same segment are equal" and "opposite angles of a
cyclic quadrilateral add to π", for oriented angles mod π (for which those are the same result),
represented here as equality of twice the angles.  -/
EuclideanGeometry.Cospherical.two_zsmul_oangle_eq : ∀ {V : Type u_3} {P : Type u_4} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {p₁ p₂ p₃ p₄ : P},
  EuclideanGeometry.Cospherical {p₁, p₂, p₃, p₄} →
    p₂ ≠ p₁ →
      p₂ ≠ p₄ → p₃ ≠ p₁ → p₃ ≠ p₄ → 2 • EuclideanGeometry.oangle p₁ p₂ p₄ = 2 • EuclideanGeometry.oangle p₁ p₃ p₄
-- Init.Core
false_iff_true : (False ↔ True) ↔ False
-- Mathlib.Topology.Algebra.PontryaginDual
PontryaginDual.instIsTopologicalGroup : ∀ {A : Type u_1} [inst : Monoid A] [inst_1 : TopologicalSpace A], IsTopologicalGroup (PontryaginDual A)
-- Mathlib.Data.ZMod.Basic
ZMod.cast.eq_2 : ∀ {R : Type u_1} [inst : AddGroupWithOne R] (n : ℕ), ZMod.cast = fun i => ↑i.val