mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.MonoidLocalization.Maps
Submonoid.LocalizationMap.ofMulEquivOfLocalizations_comp : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N] {P : Type u_3}
  [inst_2 : CommMonoid P] (f : S.LocalizationMap N) {Q : Type u_4} [inst_3 : CommMonoid Q] {k : N ≃* P} {j : P ≃* Q},
  (f.ofMulEquivOfLocalizations (k.trans j)).toMonoidHom = j.toMonoidHom.comp (f.ofMulEquivOfLocalizations k).toMonoidHom
-- Mathlib.Analysis.LocallyConvex.Basic
Absorbs.exists_pos : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : SeminormedRing 𝕜] [inst_1 : SMul 𝕜 E] {A B : Set E},
  Absorbs 𝕜 A B → ∃ r > 0, ∀ (c : 𝕜), r ≤ ‖c‖ → B ⊆ c • A
-- Mathlib.Algebra.Category.ModuleCat.ExteriorPower
/-- Constructor for elements in `M.exteriorPower n` when `M` is an object of `ModuleCat R`
and `n : ℕ`.  -/
ModuleCat.exteriorPower.mk : {R : Type u} → [inst : CommRing R] → {M : ModuleCat R} → {n : ℕ} → M.AlternatingMap (M.exteriorPower n) n
-- Std.Data.Iterators.Lemmas.Equivalence.StepCongr
Std.IterM.Equiv.eq_1 : ∀ {m : Type w → Type w'} [inst : Monad m] [inst_1 : LawfulMonad m] {β α₁ α₂ : Type w} [inst_2 : Std.Iterator α₁ m β]
  [inst_3 : Std.Iterator α₂ m β] (ita : Std.IterM m β) (itb : Std.IterM m β),
  ita.Equiv itb = Std.BundledIterM.Equiv m β (Std.BundledIterM.ofIterM ita) (Std.BundledIterM.ofIterM itb)
-- Mathlib.GroupTheory.GroupAction.ConjAct
ConjAct.card : ∀ {G : Type u_3} [inst : Fintype G], Fintype.card (ConjAct G) = Fintype.card G
-- Mathlib.Algebra.Order.Ring.Synonym
OrderDual.instNonUnitalCommSemiring : {R : Type u_1} → [NonUnitalCommSemiring R] → NonUnitalCommSemiring Rᵒᵈ
-- Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
RootPairing.PolarizationIn_eq : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) (S : Type u_5)
  [inst_5 : CommRing S] [inst_6 : Algebra S R] [inst_7 : FaithfulSMul S R] [inst_8 : Module S M]
  [inst_9 : IsScalarTower S R M] [inst_10 : Module S N] [IsScalarTower S R N] [inst_12 : P.IsValuedIn S]
  [inst_13 : Fintype ι] (x : ↥(P.rootSpan S)), (P.PolarizationIn S) x = P.Polarization ↑x
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
/-- When the second map `S.g` is zero, this is the right homology data on `S` given
by the chosen `cokernel S.f`  -/
CategoryTheory.ShortComplex.RightHomologyData.ofHasCokernel : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      (S : CategoryTheory.ShortComplex C) → [CategoryTheory.Limits.HasCokernel S.f] → S.g = 0 → S.RightHomologyData
-- Mathlib.Analysis.Complex.Convex
convex_halfSpace_im_gt : ∀ (r : ℝ), Convex ℝ {c | r < c.im}
-- Mathlib.Data.Fintype.Sum
Finset.toRight_univ : ∀ {α : Type u_3} {β : Type u_4} [inst : Fintype α] [inst_1 : Fintype β], Finset.univ.toRight = Finset.univ
-- Mathlib.Algebra.Colimit.Ring
Ring.DirectLimit.congr_symm_apply_of : ∀ {ι : Type u_1} [inst : Preorder ι] {G : ι → Type u_2} [inst_1 : (i : ι) → CommRing (G i)]
  {f : (i j : ι) → i ≤ j → G i →+* G j} {G' : ι → Type u_4} [inst_2 : (i : ι) → CommRing (G' i)]
  {f' : (i j : ι) → i ≤ j → G' i →+* G' j} (e : (i : ι) → G i ≃+* G' i)
  (he : ∀ (i j : ι) (h : i ≤ j), (e j).toRingHom.comp (f i j h) = (f' i j h).comp ↑(e i)) {i : ι} (g : G' i),
  (Ring.DirectLimit.congr e he).symm ((Ring.DirectLimit.of G' (fun x x_1 h => ⇑(f' x x_1 h)) i) g) =
    (Ring.DirectLimit.of G (fun x x_1 h => ⇑(f x x_1 h)) i) ((e i).symm g)
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.isLongestRevMatchAt_of_ofSliceFrom : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice} {p : s.Pos}
  {startPos endPos : (s.sliceFrom p).Pos},
  String.Slice.Pattern.Model.IsLongestRevMatchAt pat (String.Slice.Pos.ofSliceFrom startPos)
      (String.Slice.Pos.ofSliceFrom endPos) →
    String.Slice.Pattern.Model.IsLongestRevMatchAt pat startPos endPos
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.Walk.adj_of_length_eq_one : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v}, p.length = 1 → G.Adj u v
-- Mathlib.Probability.Distributions.Beta
/-- The beta pdf is strongly measurable.  -/
ProbabilityTheory.stronglyMeasurable_betaPDFReal : ∀ (α β : ℝ), MeasureTheory.StronglyMeasurable (ProbabilityTheory.betaPDFReal α β)
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
/-- Given a `k`-module `A` with a compatible `DistribMulAction` of `G`, and a term
`x : A` satisfying the 0-boundary condition, this produces an element of the kernel of the quotient
map `A → A_G` for the representation on `A` induced by the `DistribMulAction`.  -/
groupHomology.coinvariantsKerOfIsBoundary₀ : {k G A : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] →
      [inst_2 : AddCommGroup A] →
        [inst_3 : Module k A] →
          [inst_4 : DistribMulAction G A] →
            [inst_5 : SMulCommClass G k A] →
              (x : A) →
                groupHomology.IsBoundary₀ G x →
                  ↥(Representation.Coinvariants.ker (Representation.ofDistribMulAction k G A))
-- Mathlib.Algebra.Category.Grp.FilteredColimits
AddGrpCat.FilteredColimits.colimitAddGroup : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    [inst_1 : CategoryTheory.IsFiltered J] →
      (F : CategoryTheory.Functor J AddGrpCat) → AddGroup ↑(AddGrpCat.FilteredColimits.G F)
-- Mathlib.CategoryTheory.IsConnected
CategoryTheory.Zigzag.of_zag_trans : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {j₁ j₂ j₃ : J},
  CategoryTheory.Zag j₁ j₂ → CategoryTheory.Zag j₂ j₃ → CategoryTheory.Zigzag j₁ j₃
-- Mathlib.Algebra.Group.Subgroup.Ker
AddMonoidHom.domRestrict_range : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] (K : AddSubgroup G) (f : G →+ N),
  (f.domRestrict K).range = AddSubgroup.map f K
-- Mathlib.Algebra.Group.WithOne.Defs
WithOne.instMul.eq_1 : ∀ {α : Type u} [inst : Mul α], WithOne.instMul = { mul := Option.merge fun x1 x2 => x1 * x2 }
-- Mathlib.Algebra.Ring.Subsemiring.Basic
RingHom.codRestrict_apply : ∀ {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] {σS : Type u_2}
  [inst_2 : SetLike σS S] [inst_3 : SubsemiringClass σS S] (f : R →+* S) (s : σS) (h : ∀ (x : R), f x ∈ s) (x : R),
  ↑((f.codRestrict s h) x) = f x
-- Mathlib.Analysis.BoxIntegral.Partition.Filter
BoxIntegral.IntegrationParams.RCond.mono : ∀ {l₁ l₂ : BoxIntegral.IntegrationParams} {ι : Type u_2} {r : (ι → ℝ) → ↑(Set.Ioi 0)}, l₁ ≤ l₂ → l₂.RCond r → l₁.RCond r
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Complex.cos_sub_nat_mul_two_pi : ∀ (x : ℂ) (n : ℕ), Complex.cos (x - ↑n * (2 * ↑Real.pi)) = Complex.cos x
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace
AlgebraicGeometry.LocallyRingedSpace.Hom.toHom : {X Y : AlgebraicGeometry.LocallyRingedSpace} → X.Hom Y → X.Hom Y.toPresheafedSpace
-- Mathlib.Order.Defs.Unbundled
Equivalence.stdRefl : ∀ {α : Sort u_1} (r : α → α → Prop), Equivalence r → Std.Refl r
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.MonoidalCategory.leftUnitor_monoidal : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X₁ X₂ : C),
  CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.leftUnitor X₁).hom
      (CategoryTheory.MonoidalCategoryStruct.leftUnitor X₂).hom =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.tensorμ (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) X₁
        (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) X₂)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight
          (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).hom
          (CategoryTheory.MonoidalCategoryStruct.tensorObj X₁ X₂))
        (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorObj X₁ X₂)).hom)
-- Init.Data.Array.Monadic
_private.Init.Data.Array.Monadic.0.Array.filterMapM.match_1.eq_1 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (b : β) (h_1 : (b : β) → motive (some b)) (h_2 : Unit → motive none),
  (match some b with
    | some b => h_1 b
    | none => h_2 ()) =
    h_1 b
-- Lean.Meta.Basic
Lean.Meta.instInhabitedInfoCacheKey : Inhabited Lean.Meta.InfoCacheKey
-- Mathlib.Algebra.Order.Hom.MonoidWithZero
OrderMonoidWithZeroHom.toOrderMonoidHom_eq_coe : ∀ {α : Type u_2} {β : Type u_3} {hα : Preorder α} {hα' : MulZeroOneClass α} {hβ : Preorder β} {hβ' : MulZeroOneClass β}
  (f : α →*₀o β), f.toOrderMonoidHom = ↑f
-- Mathlib.Data.Nat.Cast.Prod
Prod.fst_natCast : ∀ {α : Type u_1} {β : Type u_2} [inst : AddMonoidWithOne α] [inst_1 : AddMonoidWithOne β] (n : ℕ), (↑n).1 = ↑n
-- Mathlib.MeasureTheory.Integral.Lebesgue.Map
MeasureTheory.lintegral_indicator_const_comp : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {f : α → β} {s : Set β},
  Measurable f → MeasurableSet s → ∀ (c : ENNReal), ∫⁻ (a : α), s.indicator (fun x => c) (f a) ∂μ = c * μ (f ⁻¹' s)
-- Batteries.Data.List.Scan
/-- Indexing into a flattened list: `L.flatten[i]` equals `L[j][k]` where
`j` is the sublist index and `k` is the offset within that sublist.

The indices are computed as:
- `j` is one less than where the cumulative sum first exceeds `i`
- `k` is `i` minus the total length of the first `j` sublists

This theorem states that these indices are in range and the equality holds.
 -/
List.getElem_flatten : ∀ {α : Type u_1} (L : List (List α)) (i : ℕ) (h : i < L.flatten.length),
  L.flatten[i] =
    let j := List.findIdx (fun x => decide (x > i)) (List.map List.length L).partialSums - 1;
    have hj := ⋯;
    let k := i - (List.take j L).flatten.length;
    have hk := ⋯;
    L[j][k]
-- Mathlib.Order.Monotone.Monovary
AntivaryOn.dual : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β}
  {s : Set ι}, AntivaryOn f g s → AntivaryOn (⇑OrderDual.toDual ∘ f) (⇑OrderDual.toDual ∘ g) s
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
WeierstrassCurve.Affine.evalEval_polynomialY : ∀ {R : Type r} [inst : CommRing R] {W : WeierstrassCurve.Affine R} (x y : R),
  Polynomial.evalEval x y W.polynomialY = 2 * y + W.a₁ * x + W.a₃
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
mfderivWithin_sumSwap : ∀ {𝕜 : 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] {M' : Type u_21} [inst_6 : TopologicalSpace M']
  [inst_7 : ChartedSpace H M'] {p : M ⊕ M'} {s : Set (M ⊕ M')},
  UniqueMDiffAt[s] p → mfderiv[s] Sum.swap p = ContinuousLinearMap.id 𝕜 (TangentSpace I p)
-- Mathlib.Topology.Separation.Hausdorff
Filter.Tendsto.limUnder_eq : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [T2Space X] {x : X} {f : Filter Y} [f.NeBot] {g : Y → X},
  Filter.Tendsto g f (nhds x) → f.limUnder g = x
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey?_inter_of_mem_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k : α}, k ∈ t₂ → (t₁ ∩ t₂).getKey? k = t₁.getKey? k
-- Mathlib.Probability.ProbabilityMassFunction.Constructions
PMF.toMeasure_map : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (p : PMF α),
  Measurable f → MeasureTheory.Measure.map f p.toMeasure = (PMF.map f p).toMeasure
-- Init.Grind.Ring.Field
Lean.Grind.Field.div_zero : ∀ {α : Type u_1} [inst : Lean.Grind.Field α] {x : α}, x / 0 = 0
-- Init.Data.SInt.Lemmas
Int16.toInt8_toInt64 : ∀ (n : Int16), n.toInt64.toInt8 = n.toInt8
-- Mathlib.Tactic.ApplyFun
/-- Failure message for `applyFunTarget`.  -/
Mathlib.Tactic.applyFunTargetFailure : Lean.Term → Lean.MetaM (List Lean.MVarId)
-- Lean.Parser.Basic
Lean.Parser.ParserState.keepTop : Lean.Parser.SyntaxStack → ℕ → Lean.Parser.SyntaxStack
-- Mathlib.Analysis.Calculus.ImplicitFunction.Bivariate
/-- Implicit function `ψ : E₁ → E₂` associated with the (curried) bivariate function
`f : E₁ → E₂ → F` at `u : E₁ × E₂`.  -/
implicitFunctionOfBivariate : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    [IsRCLikeNormedField 𝕜] →
      {E₁ : Type u_2} →
        [inst_2 : NormedAddCommGroup E₁] →
          [inst_3 : NormedSpace 𝕜 E₁] →
            [CompleteSpace E₁] →
              {E₂ : Type u_3} →
                [inst_5 : NormedAddCommGroup E₂] →
                  [inst_6 : NormedSpace 𝕜 E₂] →
                    [CompleteSpace E₂] →
                      {F : Type u_4} →
                        [inst_8 : NormedAddCommGroup F] →
                          [inst_9 : NormedSpace 𝕜 F] →
                            [CompleteSpace F] →
                              {u : E₁ × E₂} →
                                {f : E₁ → E₂ → F} →
                                  {f₁ : E₁ → E₂ → E₁ →L[𝕜] F} →
                                    {f₂ : E₁ → E₂ → E₂ →L[𝕜] F} →
                                      (∀ᶠ (v : E₁ × E₂) in nhds u, HasFDerivAt (fun x => f x v.2) (f₁ v.1 v.2) v.1) →
                                        (∀ᶠ (v : E₁ × E₂) in nhds u, HasFDerivAt (fun x => f v.1 x) (f₂ v.1 v.2) v.2) →
                                          ContinuousAt (↿f₁) u →
                                            ContinuousAt (↿f₂) u → (f₂ u.1 u.2).IsInvertible → E₁ → E₂
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
/-- The identity `StrictlyUnitaryLaxFunctor`.  -/
CategoryTheory.StrictlyUnitaryLaxFunctor.id : (B : Type u₁) → [inst : CategoryTheory.Bicategory B] → CategoryTheory.StrictlyUnitaryLaxFunctor B B
-- Batteries.Recycling.RBTree.Lemmas
/-- A statement of the greatest-ness of the result of `lowerBoundP?`. If `x` is the return value of
`lowerBoundP?` and it is strictly less than the cut, then any other `y > x` in the tree is in fact
strictly greater than the cut (so there is no exact match, and nothing closer to the cut).
 -/
RBTree.RBSet.lowerBoundP?_greatest : ∀ {α : Type u_1} {cmp : α → α → Ordering} {cut : α → Ordering} {x y : α} {t : RBTree.RBSet α cmp} [Std.TransCmp cmp]
  [RBTree.RBNode.IsCut cmp cut],
  t.lowerBoundP? cut = some x → y ∈ t → cmp x y = Ordering.lt → cut x = Ordering.gt → cut y = Ordering.lt
-- Mathlib.Analysis.Asymptotics.Defs
/-- The Landau notation `f =O[l] g` where `f` and `g` are two functions on a type `α` and `l` is
a filter on `α`, means that eventually for `l`, `‖f‖` is bounded by a constant multiple of `‖g‖`.
In other words, `‖f‖ / ‖g‖` is eventually bounded, modulo division by zero issues that are avoided
by this definition.  -/
Asymptotics.IsBigO : {α : Type u_18} → {E : Type u_19} → {F : Type u_20} → [Norm E] → [Norm F] → Filter α → (α → E) → (α → F) → Prop
-- Lean.Elab.Arg
/-- Overrides the binder infos for the first `numImplicitParams` parameters
to make them be implicit if they were explicit.
This is used for expanding projection notation. The primary motivation for this field
is that class projections may feature explicit structure parameters.
See the note at `Lean.Elab.Term.ElabAppArgs.processExplicitArg`.  -/
Lean.Elab.Term.NamedArg.numImplicitParams : Lean.Elab.Term.NamedArg → ℕ
-- Mathlib.RingTheory.Teichmuller
Perfection.mk_comp_teichmuller : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)] {R : Type u_1} [inst_1 : CommRing R] (I : Ideal R) [inst_2 : CharP (R ⧸ I) p]
  [inst_3 : IsAdicComplete I R],
  (↑(Ideal.Quotient.mk I)).comp (Perfection.teichmuller p I) = ↑(Perfection.coeff (R ⧸ I) p 0)
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.BoundedFormula.rel : {L : FirstOrder.Language} →
  {α : Type u'} → {n l : ℕ} → L.Relations l → (Fin l → L.Term (α ⊕ Fin n)) → L.BoundedFormula α n
-- Mathlib.Order.Category.Preord
Preord.Hom.ext_iff : ∀ {X Y : Preord} {x y : X.Hom Y}, x = y ↔ x.hom' = y.hom'
-- Mathlib.Topology.MetricSpace.Completion
UniformSpace.Completion.instIsBoundedSMul : ∀ {α : Type u} [inst : PseudoMetricSpace α] {M : Type u_1} [inst_1 : Zero M] [inst_2 : Zero α] [inst_3 : SMul M α]
  [inst_4 : PseudoMetricSpace M] [IsBoundedSMul M α], IsBoundedSMul M (UniformSpace.Completion α)
-- Mathlib.NumberTheory.Real.Irrational
Irrational.of_sub_natCast : ∀ {x : ℝ} (m : ℕ), Irrational (x - ↑m) → Irrational x
-- Mathlib.RingTheory.Ideal.Quotient.Operations
DoubleQuot.quotQuotEquivComm_symmₐ : ∀ (R : Type u) {A : Type u_1} [inst : CommSemiring R] [inst_1 : CommRing A] [inst_2 : Algebra R A] (I J : Ideal A),
  (DoubleQuot.quotQuotEquivCommₐ R I J).symm = DoubleQuot.quotQuotEquivCommₐ R J I
-- Lean.MetavarContext
/-- Return true iff the given level contains an assigned metavariable.  -/
Lean.hasAssignedLevelMVar : {m : Type → Type} → [Monad m] → [Lean.MonadMCtx m] → Lean.Level → m Bool
-- Mathlib.CategoryTheory.Limits.Types.Colimits
CategoryTheory.Limits.Types.hasColimit_iff_small_colimitType : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J (Type u)),
  CategoryTheory.Limits.HasColimit F ↔ Small.{u, max u v} F.ColimitType
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.biprod.inr_desc : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {W X Y : C} [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X Y] (f : X ⟶ W) (g : Y ⟶ W),
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr (CategoryTheory.Limits.biprod.desc f g) = g
-- Mathlib.Topology.Instances.TrivSqZeroExt
TrivSqZeroExt.nhds_def : ∀ {R : Type u_3} {M : Type u_4} [inst : TopologicalSpace R] [inst_1 : TopologicalSpace M] (x : TrivSqZeroExt R M),
  nhds x = nhds x.fst ×ˢ nhds x.snd
-- Mathlib.Order.Filter.AtTopBot.Tendsto
/-- A function `f` goes to `∞` independent of an order-preserving embedding `e`.  -/
Filter.tendsto_atTop_embedding : ∀ {α : Type u_3} {β : Type u_4} {γ : Type u_5} [inst : Preorder β] [inst_1 : Preorder γ] {f : α → β} {e : β → γ}
  {l : Filter α},
  (∀ (b₁ b₂ : β), e b₁ ≤ e b₂ ↔ b₁ ≤ b₂) →
    (∀ (c : γ), ∃ b, c ≤ e b) → (Filter.Tendsto (e ∘ f) l Filter.atTop ↔ Filter.Tendsto f l Filter.atTop)
-- Mathlib.CategoryTheory.Limits.Shapes.Equivalence
CategoryTheory.hasTerminal_of_equivalence : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : CategoryTheory.Functor D C) [e.IsEquivalence] [CategoryTheory.Limits.HasTerminal C],
  CategoryTheory.Limits.HasTerminal D
-- Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
SSet.relativeCellComplexCellsEquiv_apply : ∀ {X : SSet} (c : X.relativeCellComplex.Cells), SSet.relativeCellComplexCellsEquiv c = SSet.N.mk c.k.simplex ⋯
-- Mathlib.GroupTheory.GroupAction.DomAct.ActionHom
DomMulAct.mk_smul_mulActionHom_apply : ∀ {M : Type u_1} {α : Type u_2} {N : Type u_3} {β : Type u_4} [inst : SMul M α] [inst_1 : SMul N α]
  [inst_2 : SMulCommClass M N α] [inst_3 : SMul N β] (c : M) (f : α →ₑ[id] β) (a : α),
  (DomMulAct.mk c • f) a = f (c • a)
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
IsUnit.cfcRpow : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : Ring A] [inst_2 : StarRing A] [inst_3 : TopologicalSpace A]
  [inst_4 : StarOrderedRing A] [inst_5 : Algebra ℝ A] [inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint]
  [inst_7 : NonnegSpectrumClass ℝ A] {a : A},
  IsUnit a → ∀ (x : ℝ), autoParam (0 ≤ a) IsUnit.cfcRpow._auto_1 → IsUnit (a ^ x)
-- Mathlib.Order.Monotone.Monovary
monovary_toDual_left : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β},
  Monovary (⇑OrderDual.toDual ∘ f) g ↔ Antivary f g
-- Mathlib.LinearAlgebra.Matrix.WithConv
Matrix.isSymm_iff_intrinsicStar_toLin' : ∀ {n : Type u_2} {α : Type u_3} [inst : CommSemiring α] [inst_1 : StarRing α] [inst_2 : Fintype n]
  [inst_3 : DecidableEq n] {A : Matrix n n α},
  A.IsSymm ↔ star (WithConv.toConv (Matrix.toLin' A)) = WithConv.toConv (Matrix.toLin' (star A))
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
CategoryTheory.Functor.PullbackObjObj.mapArrowLeft_right : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  {G : CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂)} {f₁ f₁' : CategoryTheory.Arrow C₁}
  {f₃ : CategoryTheory.Arrow C₃} (sq₁₃ : G.PullbackObjObj f₁.hom f₃.hom) (sq₁₃' : G.PullbackObjObj f₁'.hom f₃.hom)
  (sq : f₁' ⟶ f₁),
  (sq₁₃.mapArrowLeft sq₁₃' sq).right =
    ⋯.lift (CategoryTheory.CategoryStruct.comp sq₁₃.fst ((G.map (CategoryTheory.Arrow.Hom.left sq).op).app f₃.left))
      (CategoryTheory.CategoryStruct.comp sq₁₃.snd ((G.map (CategoryTheory.Arrow.Hom.right sq).op).app f₃.right)) ⋯
-- Mathlib.MeasureTheory.Measure.Prod
MeasureTheory.QuasiMeasurePreserving.fst : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  [inst_2 : MeasurableSpace γ] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} {τ : MeasureTheory.Measure γ}
  {f : α → β × γ},
  MeasureTheory.Measure.QuasiMeasurePreserving f μ (ν.prod τ) →
    MeasureTheory.Measure.QuasiMeasurePreserving (fun x => (f x).1) μ ν
-- Mathlib.Geometry.Manifold.ContMDiff.Constructions
extChartAt_inr_apply : ∀ {𝕜 : 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] {M' : Type u_16} [inst_6 : TopologicalSpace M']
  [inst_7 : ChartedSpace H M'] {x y : M'}, ↑(extChartAt I (Sum.inr x)) (Sum.inr y) = ↑(extChartAt I x) y
-- Mathlib.LinearAlgebra.TensorProduct.Basic
TensorProduct.comm_comp_comm_assoc : ∀ (R : Type u_1) [inst : CommSemiring R] (M : Type u_7) (N : Type u_8) {P : Type u_9} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : Module R P] (f : P →ₗ[R] TensorProduct R M N),
  ↑(TensorProduct.comm R N M) ∘ₗ ↑(TensorProduct.comm R M N) ∘ₗ f = f
-- Lean.Meta.Match.MatcherInfo
Lean.Meta.Match.instReprMatcherInfo.repr : Lean.Meta.MatcherInfo → ℕ → Std.Format
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.Const.get?.match_1.splitter : {α : Type u_1} →
  {δ : Type u_2} →
    (motive : (Std.DTreeMap.Internal.Impl α fun x => δ) → Sort u_3) →
      (t : Std.DTreeMap.Internal.Impl α fun x => δ) →
        (Unit → motive Std.DTreeMap.Internal.Impl.leaf) →
          ((size : ℕ) →
              (k' : α) →
                (v' : δ) →
                  (l r : Std.DTreeMap.Internal.Impl α fun x => δ) →
                    motive (Std.DTreeMap.Internal.Impl.inner size k' v' l r)) →
            motive t
-- Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
/-- The ring isomorphism `v.Completion ≃+* ℂ`, when `v` is complex, given by the bijection
`v.Completion →+* ℂ`.  -/
NumberField.InfinitePlace.Completion.ringEquivComplexOfIsComplex : {K : Type u_1} → [inst : Field K] → {v : NumberField.InfinitePlace K} → v.IsComplex → v.Completion ≃+* ℂ
-- Mathlib.Data.WSeq.Defs
/-- Select the elements of `s` that satisfy `p`.  -/
Stream'.WSeq.filter : {α : Type u} → (p : α → Prop) → [DecidablePred p] → Stream'.WSeq α → Stream'.WSeq α
-- Mathlib.Algebra.Module.Torsion.Basic
Submodule.QuotientTorsion.instIsTorsionFree : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsDomain R],
  Module.IsTorsionFree R (M ⧸ Submodule.torsion R M)
-- Lean.Meta.Sym.Arith.Types
Lean.Meta.Sym.Arith.RingExpr : Type
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.Internal.List.Const.beqModel.eq_1 : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : BEq β] (l₁ l₂ : List ((_ : α) × β)),
  Std.Internal.List.Const.beqModel l₁ l₂ =
    if l₁.length ≠ l₂.length then false else l₁.all fun x => Std.Internal.List.getValue? x.fst l₂ == some x.snd