mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Shift.Adjunction
CategoryTheory.Adjunction.RightAdjointCommShift.iso_hom_app_assoc : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  (adj : F ⊣ G) {A : Type u_3} [inst_2 : AddGroup A] [inst_3 : CategoryTheory.HasShift C A]
  [inst_4 : CategoryTheory.HasShift D A] (a b : A) (h : b + a = 0) [inst_5 : F.CommShift A] (X : D) {Z : C}
  (h_1 : (CategoryTheory.shiftFunctor C a).obj (G.obj X) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.Adjunction.RightAdjointCommShift.iso adj a).hom.app X) h_1 =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.shiftFunctorCompIsoId C b a h).inv.app (G.obj ((CategoryTheory.shiftFunctor D a).obj X)))
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.shiftFunctor C a).map
          (adj.unit.app ((CategoryTheory.shiftFunctor C b).obj (G.obj ((CategoryTheory.shiftFunctor D a).obj X)))))
        (CategoryTheory.CategoryStruct.comp
          ((CategoryTheory.shiftFunctor C a).map
            (G.map
              ((CategoryTheory.Functor.commShiftIso F b).hom.app (G.obj ((CategoryTheory.shiftFunctor D a).obj X)))))
          (CategoryTheory.CategoryStruct.comp
            ((CategoryTheory.shiftFunctor C a).map
              (G.map
                ((CategoryTheory.shiftFunctor D b).map (adj.counit.app ((CategoryTheory.shiftFunctor D a).obj X)))))
            (CategoryTheory.CategoryStruct.comp
              ((CategoryTheory.shiftFunctor C a).map (G.map ((CategoryTheory.shiftFunctorCompIsoId D a b ⋯).hom.app X)))
              h_1))))
-- Mathlib.Analysis.Calculus.Gradient.Basic
toDual_gradientWithin : ∀ {𝕜 : Type u_1} {F : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup F] [inst_2 : InnerProductSpace 𝕜 F]
  [inst_3 : CompleteSpace F] {f : F → 𝕜} {x : F} {s : Set F},
  (InnerProductSpace.toDual 𝕜 F) (gradientWithin f s x) = fderivWithin 𝕜 f s x
-- Lean.Declaration
Lean.DefinitionSafety.partial : Lean.DefinitionSafety
-- Mathlib.MeasureTheory.Measure.Typeclasses.NullSingletonClass
MeasureTheory.Iio_ae_eq_Iic : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.NullSingletonClass μ]
  [inst : PartialOrder α] {a : α}, Set.Iio a =ᵐ[μ] Set.Iic a
-- Std.Data.HashSet.Lemmas
Std.HashSet.size_ofList : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List α},
  List.Pairwise (fun a b => (a == b) = false) l → (Std.HashSet.ofList l).size = l.length
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
/-- Append `Fin m ↪ ofFixingSubgroup M s` at the end of an enumeration of `s`.  -/
SubMulAction.ofFixingSubgroup.append : {M : Type u_1} →
  {α : Type u_2} →
    [inst : Group M] →
      [inst_1 : MulAction M α] →
        {s : Set α} → {n : ℕ} → [Finite ↑s] → (Fin n ↪ ↥(SubMulAction.ofFixingSubgroup M s)) → Fin (s.ncard + n) ↪ α
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.Walk.end_mem_support : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v), v ∈ p.support
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.LeftHomologyData.ofHasKernelOfHasCokernel_π : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : CategoryTheory.Limits.HasKernel S.g]
  [inst_3 : CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.kernel.lift S.g S.f ⋯)],
  (CategoryTheory.ShortComplex.LeftHomologyData.ofHasKernelOfHasCokernel S).π =
    CategoryTheory.Limits.cokernel.π (CategoryTheory.Limits.kernel.lift S.g S.f ⋯)
-- Mathlib.Order.Interval.Finset.Defs
Finset.map_subtype_embedding_Ioc : ∀ {α : Type u_1} [inst : Preorder α] (p : α → Prop) [inst_1 : DecidablePred p] [inst_2 : LocallyFiniteOrder α]
  (a b : Subtype p),
  (∀ ⦃a b x : α⦄, a ≤ x → x ≤ b → p a → p b → p x) →
    Finset.map (Function.Embedding.subtype p) (Finset.Ioc a b) = Finset.Ioc ↑a ↑b
-- Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed
AlgebraicGeometry.universallyClosed_isZariskiLocalAtTarget : AlgebraicGeometry.IsZariskiLocalAtTarget @AlgebraicGeometry.UniversallyClosed
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
/-- **Alias** of `Left.add_neg`.  -/
add_neg : ∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α] [AddLeftStrictMono α] {a b : α},
  a < 0 → b < 0 → a + b < 0
-- Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
CategoryTheory.Limits.initial.strict_hom_ext_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasStrictInitialObjects C]
  [inst_2 : CategoryTheory.Limits.HasInitial C] {A : C} {f g : A ⟶ ⊥_ C}, f = g ↔ True
-- Mathlib.Topology.MetricSpace.Isometry
/-- Isometries preserve the diameter in pseudoemetric spaces.  -/
Isometry.ediam_image : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {f : α → β},
  Isometry f → ∀ (s : Set α), Metric.ediam (f '' s) = Metric.ediam s
-- Mathlib.Algebra.Quaternion
Quaternion.im_neg : ∀ {R : Type u_3} [inst : CommRing R] (a : Quaternion R), (-a).im = -a.im
-- Mathlib.RepresentationTheory.Continuous.TopRep
TopRep.hom_comm_apply : ∀ {k : Type u} {G : Type v} [inst : TopologicalSpace k] [inst_1 : Ring k] [inst_2 : Monoid G] {A B : TopRep k G}
  (f : A ⟶ B) (g : G) (a : ↑A), (TopRep.Hom.hom f) ((A.ρ g) a) = (B.ρ g) ((TopRep.Hom.hom f) a)
-- Std.Http.Server.Connection
_private.Std.Http.Server.Connection.0.Std.Http.Server.Connection.Recv.bytes.inj : ∀ {β : Type} {x x_1 : Option ByteArray},
  Std.Http.Server.Connection.Recv.bytes✝ x = Std.Http.Server.Connection.Recv.bytes✝ x_1 → x = x_1
-- Mathlib.Topology.Instances.NNReal.Lemmas
NNReal.summable_mk : ∀ {α : Type u_2} {L : SummationFilter α} {f : α → ℝ} (hf : ∀ (n : α), 0 ≤ f n),
  Summable (fun n => ⟨f n, ⋯⟩) L ↔ Summable f L
-- Mathlib.Data.PNat.Equiv
Equiv.pnatEquivNat_symm_apply : ⇑Equiv.pnatEquivNat.symm = Nat.succPNat
-- Mathlib.Topology.Algebra.Valued.WithZeroMulInt
Valued.tendsto_zero_pow_of_v_lt_one : ∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : Ring R] [inst_1 : LinearOrderedCommGroupWithZero Γ₀] [MulArchimedean Γ₀]
  [inst_3 : Valued R Γ₀] {x : R}, Valued.v x < 1 → Filter.Tendsto (fun n => x ^ n) Filter.atTop (nhds 0)
-- Mathlib.LinearAlgebra.Multilinear.Basic
/-- When `ι` is finite, multilinear maps on `R^ι` with values in `M₂` are in bijection with `M₂`,
as such a multilinear map is completely determined by its value on the constant vector made of ones.
We register this bijection as a linear equivalence in `MultilinearMap.piRingEquiv`.  -/
MultilinearMap.piRingEquiv : {R : Type uR} →
  {ι : Type uι} →
    {M₂ : Type v₂} →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid M₂] → [inst_2 : Module R M₂] → [Fintype ι] → M₂ ≃ₗ[R] MultilinearMap R (fun x => R) M₂
-- Mathlib.Data.DFinsupp.NeLocus
DFinsupp.neLocus_self_add_left : ∀ {α : Type u_1} {N : α → Type u_2} [inst : DecidableEq α] [inst_1 : (a : α) → DecidableEq (N a)]
  [inst_2 : (a : α) → AddGroup (N a)] (f g : Π₀ (a : α), N a), (f + g).neLocus f = g.support
-- Mathlib.Logic.Equiv.Prod
Equiv.coe_uniqueProd : ∀ {α : Type u_9} {β : Type u_10} [inst : Unique β], ⇑(Equiv.uniqueProd α β) = Prod.snd
-- Lean.Elab.DocString
Lean.Doc.instFromDocArgIdent : Lean.Doc.FromDocArg Lean.Ident
-- Mathlib.Algebra.Order.Star.Basic
/-- To construct a `StarOrderedRing` instance it suffices to show that `x ≤ y` if and only if
`y = x + star s * s` for some `s : R`.

This is provided for convenience because it holds in some common scenarios (e.g.,`ℝ≥0`, `C(X, ℝ≥0)`)
and obviates the hassle of `AddSubmonoid.closure_induction` when creating those instances.

If you are working with a `NonUnitalRing` and not a `NonUnitalSemiring`, see
`StarOrderedRing.of_nonneg_iff` for a more convenient version.
 -/
StarOrderedRing.of_le_iff : ∀ {R : Type u_1} [inst : NonUnitalSemiring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R],
  (∀ (x y : R), x ≤ y ↔ ∃ s, y = x + star s * s) → StarOrderedRing R
-- Std.Http.Data.Status
/-- 511 Network Authentication Required
 -/
Std.Http.Status.networkAuthenticationRequired : Std.Http.Status
-- Mathlib.Algebra.Order.GroupWithZero.Basic
sq_le : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] [inst_1 : Preorder M₀] {a : M₀} [PosMulMono M₀], 0 ≤ a → a ≤ 1 → a ^ 2 ≤ a
-- Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
CategoryTheory.leftExactFunctor_le_additiveFunctor : ∀ (C : Type u₁) (D : Type u₂) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Preadditive D]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D]
  [CategoryTheory.Limits.HasBinaryBiproducts C],
  CategoryTheory.leftExactFunctor C D ≤ CategoryTheory.additiveFunctor C D
-- Mathlib.Order.Hom.CompleteLattice
FrameHomClass.toInfTopHomClass : ∀ {F : Type u_8} {α : Type u_9} {β : Type u_10} {inst : CompleteLattice α} {inst_1 : CompleteLattice β}
  {inst_2 : FunLike F α β} [self : FrameHomClass F α β], InfTopHomClass F α β
-- Mathlib.LinearAlgebra.Matrix.SemiringInverse
Matrix.detp_mul : ∀ {n : Type u_1} {R : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommSemiring R]
  (A B : Matrix n n R),
  Matrix.detp 1 (A * B) + (Matrix.detp 1 A * Matrix.detp (-1) B + Matrix.detp (-1) A * Matrix.detp 1 B) =
    Matrix.detp (-1) (A * B) + (Matrix.detp 1 A * Matrix.detp 1 B + Matrix.detp (-1) A * Matrix.detp (-1) B)
-- Mathlib.Topology.Instances.ENNReal.Lemmas
ENNReal.tendsto_toReal_iff : ∀ {ι : Type u_4} {fi : Filter ι} {f : ι → ENNReal},
  (∀ (i : ι), f i ≠ ⊤) →
    ∀ {x : ENNReal}, x ≠ ⊤ → (Filter.Tendsto (fun n => (f n).toReal) fi (nhds x.toReal) ↔ Filter.Tendsto f fi (nhds x))
-- Mathlib.RingTheory.Ideal.Norm.RelNorm
/-- See `Ideal.relNorm_eq_pow_of_isMaximal` for a more precise statement when `p` is a maximal ideal.
 -/
Ideal.exists_relNorm_eq_pow_of_isPrime : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] {S : Type u_3} [inst_2 : CommRing S] [inst_3 : IsDomain S]
  [inst_4 : IsIntegrallyClosed R] [inst_5 : IsIntegrallyClosed S] [inst_6 : Algebra R S] [inst_7 : Module.Finite R S]
  [inst_8 : Module.IsTorsionFree R S] [inst_9 : IsDedekindDomain R] [inst_10 : IsDedekindDomain S] (P : Ideal S)
  (p : Ideal R) [hPp : P.LiesOver p] [p.IsPrime], ∃ s, (Ideal.relNorm R) P = p ^ s
-- Mathlib.RingTheory.UniqueFactorizationDomain.Defs
WfDvdMonoid.exists_irreducible_factor : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [WfDvdMonoid α] {a : α}, ¬IsUnit a → a ≠ 0 → ∃ i, Irreducible i ∧ i ∣ a
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.isZero_E_of_isZero_H : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ),
  CategoryTheory.Limits.IsZero ((X.H n₁).obj (CategoryTheory.ComposableArrows.mk₁ f₂)) →
    ∀ (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.isZero_E_of_isZero_H._auto_1)
      (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.isZero_E_of_isZero_H._auto_3),
      CategoryTheory.Limits.IsZero (X.E f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯)
-- Mathlib.Data.Int.GCD
Nat.gcdA_zero_right : ∀ {s : ℕ}, s ≠ 0 → s.gcdA 0 = 1
-- Mathlib.Combinatorics.Graph.Subgraph
Graph.IsClosedSubgraph.mk' : ∀ {α : Type u_1} {β : Type u_2} {G H : Graph α β},
  H ≤ G → (∀ ⦃e : β⦄ ⦃x : α⦄, G.Inc e x → x ∈ H.vertexSet → e ∈ H.edgeSet) → H.IsClosedSubgraph G
-- Mathlib.MeasureTheory.OuterMeasure.Induced
/-- Given an outer measure `m` we can forget its value on non-measurable sets, and then consider
`m.trim`, the unique maximal outer measure less than that function.  -/
MeasureTheory.OuterMeasure.trim : {α : Type u_1} → [MeasurableSpace α] → MeasureTheory.OuterMeasure α → MeasureTheory.OuterMeasure α
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
NumberField.InfinitePlace.exists_smul_eq_of_comap_eq : ∀ {k : Type u_1} [inst : Field k] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra k K] [IsGalois k K]
  {w w' : NumberField.InfinitePlace K}, w.comap (algebraMap k K) = w'.comap (algebraMap k K) → ∃ σ, σ • w = w'
-- Init.Meta.Defs
Lean.Meta.ApplyConfig.mk.inj : ∀ {newGoals : Lean.Meta.ApplyNewGoals} {synthAssignedInstances allowSynthFailures approx : Bool}
  {newGoals_1 : Lean.Meta.ApplyNewGoals} {synthAssignedInstances_1 allowSynthFailures_1 approx_1 : Bool},
  { newGoals := newGoals, synthAssignedInstances := synthAssignedInstances, allowSynthFailures := allowSynthFailures,
        approx := approx } =
      { newGoals := newGoals_1, synthAssignedInstances := synthAssignedInstances_1,
        allowSynthFailures := allowSynthFailures_1, approx := approx_1 } →
    newGoals = newGoals_1 ∧
      synthAssignedInstances = synthAssignedInstances_1 ∧ allowSynthFailures = allowSynthFailures_1 ∧ approx = approx_1
-- Init.Data.Float.Float32
/-- Compares two floating point numbers for non-strict inequality.

This function does not reduce in the kernel. It is compiled to the C inequality operator.
 -/
Float32.decLe : (a b : Float32) → Decidable (a ≤ b)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
WeierstrassCurve.Projective.Point.instNeg : {F : Type u} → [inst : Field F] → {W : WeierstrassCurve.Projective F} → Neg W.Point
-- Init.Data.List.Find
List.findIdx_le_length : ∀ {α : Type u_1} {p : α → Bool} {xs : List α}, List.findIdx p xs ≤ xs.length
-- Mathlib.Topology.Algebra.Algebra
ContinuousAlgHom.coe_eq_id : ∀ (R : Type u_1) [inst : CommSemiring R] (A : Type u_2) [inst_1 : Semiring A] [inst_2 : TopologicalSpace A]
  [inst_3 : Algebra R A] {f : A →A[R] A}, ↑f = AlgHom.id R A ↔ f = ContinuousAlgHom.id R A
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getElem!_eq_default_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited β] {a : α}, m.contains a = false → m[a]! = default
-- Mathlib.Data.List.DropRight
/-- Drop `n` elements from the tail end of a list.  -/
List.rdrop : {α : Type u_1} → List α → ℕ → List α
-- Init.Data.Vector.Attach
Vector.getElem?_pmap : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ} {p : α → Prop} {f : (a : α) → p a → β} {xs : Vector α n} (h : ∀ a ∈ xs, p a)
  (i : ℕ), (Vector.pmap f xs h)[i]? = Option.pmap f xs[i]? ⋯
-- Init.Data.BitVec.Lemmas
BitVec.getLsbD_shiftLeft : ∀ {m i : ℕ} (x : BitVec m) (n : ℕ), (x <<< n).getLsbD i = (decide (i < m) && !decide (i < n) && x.getLsbD (i - n))
-- Init.Data.String.Lemmas.Splits
String.Slice.splits_prevn_endPos : ∀ (s : String.Slice) (n : ℕ),
  (s.endPos.prevn n).Splits (String.ofList (List.take (s.copy.toList.length - n) s.copy.toList))
    (String.ofList (List.drop (s.copy.toList.length - n) s.copy.toList))
-- Mathlib.Algebra.Order.Hom.Monoid
/-- For two ordered additive monoid morphisms `f` and `g`, their product is the
ordered additive monoid morphism sending `a` to `f a + g a`.  -/
OrderAddMonoidHom.instAddOfIsOrderedAddMonoid : {α : Type u_2} →
  {β : Type u_3} →
    [inst : AddCommMonoid α] →
      [inst_1 : Preorder α] →
        [inst_2 : AddCommMonoid β] → [inst_3 : Preorder β] → [IsOrderedAddMonoid β] → Add (α →+o β)
-- Mathlib.Algebra.Lie.BaseChange
_private.Mathlib.Algebra.Lie.BaseChange.0.LieAlgebra.ExtendScalars.bracket'_tmul : ∀ (R : Type u_1) (A : Type u_2) (L : Type u_3) (M : Type u_4) [inst : CommRing R] [inst_1 : CommRing A]
  [inst_2 : Algebra R A] [inst_3 : LieRing L] [inst_4 : LieAlgebra R L] [inst_5 : AddCommGroup M] [inst_6 : Module R M]
  [inst_7 : LieRingModule L M] [inst_8 : LieModule R L M] (s t : A) (x : L) (m : M),
  ((LieAlgebra.ExtendScalars.bracket'✝ R A L M) (s ⊗ₜ[R] x)) (t ⊗ₜ[R] m) = (s * t) ⊗ₜ[R] ⁅x, m⁆
-- Mathlib.Order.Ideal
Order.Ideal.bot_mem : ∀ {P : Type u_1} [inst : LE P] [inst_1 : OrderBot P] (s : Order.Ideal P), ⊥ ∈ s
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.max_eq_getLast_toList : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {he : t.isEmpty = false},
  t.max he = t.toList.getLast ⋯
-- Mathlib.Algebra.Homology.LeftResolution.Reduced
CategoryTheory.Abelian.LeftResolution.karoubi.π.eq_1 : ∀ {A : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_1} A] {ι : CategoryTheory.Functor C A}
  (Λ : CategoryTheory.Abelian.LeftResolution ι) [inst_2 : CategoryTheory.Preadditive C]
  [inst_3 : CategoryTheory.Preadditive A] [inst_4 : ι.Additive],
  CategoryTheory.Abelian.LeftResolution.karoubi.π Λ =
    CategoryTheory.Idempotents.whiskeringLeftObjToKaroubiFullyFaithful.preimage
      (CategoryTheory.Abelian.LeftResolution.karoubi.π' Λ)
-- Mathlib.Algebra.Group.Units.Basic
Units.inv_mul_eq_one : ∀ {α : Type u} [inst : Monoid α] {u : αˣ} {a : α}, ↑u⁻¹ * a = 1 ↔ ↑u = a
-- Mathlib.Topology.UniformSpace.UniformEmbedding
IsUniformInducing.uniformContinuous_iff : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : UniformSpace α] [inst_1 : UniformSpace β] [inst_2 : UniformSpace γ]
  {f : α → β} {g : β → γ}, IsUniformInducing g → (UniformContinuous f ↔ UniformContinuous (g ∘ f))
-- Mathlib.Data.Sym.Sym2
/-- `Sym2 α` is the symmetric square of `α`, which, in other words, is the
type of unordered pairs.

It is equivalent in a natural way to multisets of cardinality 2 (see
`Sym2.equivMultiset`).
 -/
Sym2 : Type u → Type u
-- Mathlib.Algebra.Group.PNatPowAssoc
ppow_eq_pow : ∀ {M : Type u_1} [inst : Monoid M] [inst_1 : Pow M ℕ+] [PNatPowAssoc M] (x : M) (n : ℕ+), x ^ n = x ^ ↑n
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.maxKey!_eq_getLast!_keys : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Inhabited α], t.WF → t.maxKey! = t.keys.getLast!
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap.0.Std.Iterators.Types.FilterMap.instIterator.match_1.eq_1 : ∀ {β γ : Type u_1} {n : Type u_1 → Type u_2} {f : β → Std.Iterators.PostconditionT n (Option γ)} (out : β)
  (motive : Subtype (f out).Property → Sort u_3) (h' : (f out).Property none)
  (h_1 : (h' : (f out).Property none) → motive ⟨none, h'⟩)
  (h_2 : (out' : γ) → (h' : (f out).Property (some out')) → motive ⟨some out', h'⟩),
  (match ⟨none, h'⟩ with
    | ⟨none, h'⟩ => h_1 h'
    | ⟨some out', h'⟩ => h_2 out' h') =
    h_1 h'
-- Mathlib.Analysis.CStarAlgebra.Module.Defs
/-- The Cauchy-Schwarz inequality for Hilbert C⋆-modules.  -/
CStarModule.norm_inner_le : ∀ {A : Type u_1} (E : Type u_2) [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] [inst_2 : AddCommGroup E]
  [inst_3 : Module ℂ E] [inst_4 : SMul A E] [inst_5 : Norm E] [inst_6 : CStarModule A E] [StarOrderedRing A] {x y : E},
  ‖inner A x y‖ ≤ ‖x‖ * ‖y‖
-- Mathlib.Algebra.Order.AbsoluteValue.Basic
AbsoluteValue.nonnegHomClass : ∀ {R : Type u_5} {S : Type u_6} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : PartialOrder S],
  NonnegHomClass (AbsoluteValue R S) R S
-- Mathlib.SetTheory.Ordinal.Basic
/-- Given two ordinals `α ≤ β`, then `initialSegToType α β` is the initial segment embedding of
`α.ToType` into `β.ToType`.  -/
Ordinal.initialSegToType : {α β : Ordinal.{u_1}} → α ≤ β → α.ToType ≤i β.ToType
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
_private.Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent.0.sineTerm_bound_aux : ∀ {Z : Set ℂ}, IsCompact Z → ∃ u, Summable u ∧ ∀ (j : ℕ), ∀ z ∈ Z, ‖sineTerm z j‖ ≤ u j
-- Mathlib.LinearAlgebra.LinearPMap
LinearPMap.domain_sSup : ∀ {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : Ring S] {σ : R →+* S} {E : Type u_4} [inst_2 : AddCommGroup E]
  [inst_3 : Module R E] {F : Type u_5} [inst_4 : AddCommGroup F] [inst_5 : Module S F] {c : Set (E →ₛₗ.[σ] F)}
  (hc : DirectedOn (fun x1 x2 => x1 ≤ x2) c), (LinearPMap.sSup c hc).domain = sSup (LinearPMap.domain '' c)
-- Mathlib.RingTheory.IsTensorProduct
IsTensorProduct.compl₂_linearEquiv : ∀ {R : Type u_1} [inst : CommSemiring R] {M₁ : Type u_2} {M₂ : Type u_3} {M : Type u_4} [inst_1 : AddCommMonoid M₁]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M] [inst_4 : Module R M₁] [inst_5 : Module R M₂]
  [inst_6 : Module R M] {f : M₁ →ₗ[R] M₂ →ₗ[R] M} {N₂ : Type u_7} [inst_7 : AddCommMonoid N₂] [inst_8 : Module R N₂],
  IsTensorProduct f → ∀ (e₂ : N₂ ≃ₗ[R] M₂), IsTensorProduct (f.compl₂ ↑e₂)
-- Std.Data.DHashMap.Raw
/-- Checks whether a key is present in a map and inserts a value for the key if it was not found.

If the returned `Bool` is `true`, then the returned map is unaltered. If the `Bool` is `false`, then
the returned map has a new value inserted.

Equivalent to (but potentially faster than) calling `contains` followed by `insertIfNew`.
 -/
Std.DHashMap.Raw.containsThenInsertIfNew : {α : Type u} →
  {β : α → Type v} → [BEq α] → [Hashable α] → Std.DHashMap.Raw α β → (a : α) → β a → Bool × Std.DHashMap.Raw α β
-- Mathlib.Data.ENNReal.Holder
ENNReal.HolderTriple.mk : ∀ {p q : ENNReal} {r : semiOutParam ENNReal}, p⁻¹ + q⁻¹ = r⁻¹ → p.HolderTriple q r
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.instModuleSubtypeMem : {R' : Type u_1} →
  {α : Type u_2} →
    [inst : Semiring R'] →
      [inst_1 : AddCommMonoid α] →
        [Module R' α] →
          {S' : Type u_5} → [inst_3 : SetLike S' R'] → [inst_4 : SubsemiringClass S' R'] → (s : S') → Module (↥s) α
-- Mathlib.MeasureTheory.Function.LpSpace.DomAct.Basic
DomMulAct.instIsIsometricSMulSubtypeAEEqFunMemAddSubgroupLp : ∀ {M : Type u_1} {α : Type u_3} {E : Type u_4} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E]
  {μ : MeasureTheory.Measure α} {p : ENNReal} [inst_2 : SMul M α] [inst_3 : MeasureTheory.SMulInvariantMeasure M α μ]
  [inst_4 : MeasurableConstSMul M α] [inst_5 : Fact (1 ≤ p)], IsIsometricSMul Mᵈᵐᵃ ↥(MeasureTheory.Lp E p μ)
-- Mathlib.Control.Fold
Monoid.Foldr.get.eq_1 : ∀ {α : Type u} (x : Monoid.Foldr α), x.get = ⇑(CategoryTheory.ConcreteCategory.hom x)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get_filterMap : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {γ : Type w} {t : Std.ExtDTreeMap α (fun x => β) cmp}
  [inst : Std.TransCmp cmp] {f : α → β → Option γ} {k : α} {h : k ∈ Std.ExtDTreeMap.filterMap f t},
  Std.ExtDTreeMap.Const.get (Std.ExtDTreeMap.filterMap f t) k h =
    (f (t.getKey k ⋯) (Std.ExtDTreeMap.Const.get t k ⋯)).get ⋯
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Stepwise.imp_1eqC : ∀ {α : Type u_1} {c : ℕ} [inst : Lean.Grind.CommRing α] [Lean.Grind.IsCharP α c] (ctx : Lean.Grind.CommRing.Context α)
  (lhs rhs : Lean.Grind.CommRing.Expr) (p₁ p₂ : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.Stepwise.imp_1eq_certC lhs rhs p₁ p₂ c = true →
    ↑1 * Lean.Grind.CommRing.Poly.denote ctx p₁ = Lean.Grind.CommRing.Poly.denote ctx p₂ →
      Lean.Grind.CommRing.Expr.denote ctx lhs = Lean.Grind.CommRing.Expr.denote ctx rhs
-- Mathlib.FieldTheory.Minpoly.Field
minpoly.add_algebraMap : ∀ {A : Type u_1} [inst : Field A] {B : Type u_3} [inst_1 : CommRing B] [inst_2 : Algebra A B] (x : B) (a : A),
  minpoly A (x + (algebraMap A B) a) = (minpoly A x).comp (Polynomial.X - Polynomial.C a)
-- Init.Data.Int.Linear
Int.Internal.Linear.le_norm_expr : ∀ (ctx : Int.Internal.Linear.Context) (lhs rhs : Int.Internal.Linear.Expr) (p : Int.Internal.Linear.Poly),
  Int.Internal.Linear.norm_eq_cert lhs rhs p = true →
    Int.Internal.Linear.Expr.denote ctx lhs ≤ Int.Internal.Linear.Expr.denote ctx rhs →
      Int.Internal.Linear.Poly.denote' ctx p ≤ 0
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- The cofork defined in `BinaryBicone.inrCokernelCofork` is indeed a cokernel.  -/
CategoryTheory.Limits.BinaryBicone.isColimitInrCokernelCofork : {C : Type uC} →
  [inst : CategoryTheory.Category.{uC', uC} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y : C} →
        {c : CategoryTheory.Limits.BinaryBicone X Y} →
          CategoryTheory.Limits.IsColimit c.toCocone → CategoryTheory.Limits.IsColimit c.inrCokernelCofork