mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Normed.Operator.ContinuousLinearMap
/-- Construct a continuous linear map from a linear map and a bound on this linear map.
The fact that the norm of the continuous linear map is then controlled is given in
`LinearMap.mkContinuous_norm_le`.  -/
LinearMap.mkContinuous : {𝕜 : Type u_1} →
  {𝕜₂ : Type u_2} →
    {E : Type u_3} →
      {F : Type u_4} →
        [inst : Ring 𝕜] →
          [inst_1 : Ring 𝕜₂] →
            [inst_2 : SeminormedAddCommGroup E] →
              [inst_3 : SeminormedAddCommGroup F] →
                [inst_4 : Module 𝕜 E] →
                  [inst_5 : Module 𝕜₂ F] →
                    {σ : 𝕜 →+* 𝕜₂} → (f : E →ₛₗ[σ] F) → (C : ℝ) → (∀ (x : E), ‖f x‖ ≤ C * ‖x‖) → E →SL[σ] F
-- Mathlib.RingTheory.GradedAlgebra.RingHom
/-- Graded ring homomorphisms preserve addition.  -/
GradedRingHom.map_add : ∀ {ι : Type u_1} {A : Type u_2} {B : Type u_3} {σ : Type u_6} {τ : Type u_7} [inst : Semiring A] [inst_1 : Semiring B]
  [inst_2 : SetLike σ A] [inst_3 : SetLike τ B] {𝒜 : ι → σ} {ℬ : ι → τ} (f : 𝒜 →+*ᵍ ℬ) (a b : A), f (a + b) = f a + f b
-- Mathlib.NumberTheory.Padics.RingHoms
/-- `zmodRepr x` is the unique natural number smaller than `p`
satisfying `‖(x - zmodRepr x : ℤ_[p])‖ < 1`.
 -/
PadicInt.zmodRepr : {p : ℕ} → [hp_prime : Fact (Nat.Prime p)] → ℤ_[p] → ℕ
-- Std.Data.DHashMap.RawDecidableEquiv
Std.DHashMap.Raw.instDecidableEquiv : {α : Type u} →
  {β : α → Type v} →
    [inst : BEq α] →
      [LawfulBEq α] →
        [inst_2 : Hashable α] →
          [inst_3 : (k : α) → BEq (β k)] →
            [∀ (k : α), LawfulBEq (β k)] → {m₁ m₂ : Std.DHashMap.Raw α β} → m₁.WF → m₂.WF → Decidable (m₁.Equiv m₂)
-- Mathlib.CategoryTheory.Sites.Subcanonical
/-- Two morphisms of sheaves of types `P ⟶ Q` coincide if the precompositions with morphisms
`yoneda.obj X ⟶ P` agree.
 -/
CategoryTheory.GrothendieckTopology.hom_ext_yoneda : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C)
  [inst_1 : J.Subcanonical] {P Q : CategoryTheory.Sheaf J (Type v)} {f g : P ⟶ Q},
  (∀ (X : C) (p : J.yoneda.obj X ⟶ P),
      CategoryTheory.CategoryStruct.comp p f = CategoryTheory.CategoryStruct.comp p g) →
    f = g
-- Init.Data.Range.Polymorphic.UInt
UInt32.succ?_ofBitVec : ∀ {x : BitVec 32}, Std.PRange.succ? { toBitVec := x } = UInt32.ofBitVec <$> Std.PRange.succ? x
-- Mathlib.LinearAlgebra.QuadraticForm.Dual
/-- Vectors which subtend obtuse angles with each other and all lie in the same half-space are
linearly independent.

This is [serre1965](Ch. V, §9, Lemma 4).  -/
LinearMap.BilinForm.linearIndependent_of_pairwise_le_zero : ∀ {ι : Type u_4} {R : Type u_5} {M : Type u_6} [inst : CommRing R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] (B : LinearMap.BilinForm R M),
  (LinearMap.BilinMap.toQuadraticMap B).PosDef →
    ∀ (f : Module.Dual R M) (v : ι → M),
      (∀ (i : ι), 0 < f (v i)) → (Pairwise fun i j => (B (v i)) (v j) ≤ 0) → LinearIndependent R v
-- Mathlib.Algebra.Group.Subgroup.Defs
SubgroupClass.toCommGroup.eq_1 : ∀ {S : Type u_4} (H : S) {G : Type u_5} [inst : CommGroup G] [inst_1 : SetLike S G] [inst_2 : SubgroupClass S G],
  SubgroupClass.toCommGroup H = { toGroup := SubgroupClass.toGroup H, mul_comm := ⋯ }
-- Mathlib.Order.Hom.BoundedLattice
InfTopHom.instInhabited.eq_1 : ∀ (α : Type u_2) [inst : Min α] [inst_1 : Top α], InfTopHom.instInhabited α = { default := InfTopHom.id α }
-- Init.Data.AC
Lean.Data.AC.insert_nonEmpty : ∀ {x : ℕ} {xs : List ℕ}, Lean.Data.AC.insert x xs ≠ []
-- Batteries.Data.List.Basic
/-- Get the minimum element of a list.
If the given list is empty, returns `(default : α)` and produces a panic error message.  -/
List.min! : {α : Type u_1} → [Inhabited α] → [Min α] → List α → α
-- Mathlib.Analysis.Convex.Basic
convex_openSegment : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : CommSemiring 𝕜] [inst_1 : PartialOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] (a b : E), Convex 𝕜 (openSegment 𝕜 a b)
-- Mathlib.GroupTheory.Torsion
/-- Additive subgroups of torsion additive groups are torsion additive groups.  -/
IsAddTorsion.addSubgroup : ∀ {G : Type u_1} [inst : AddGroup G], IsAddTorsion G → ∀ (H : AddSubgroup G), IsAddTorsion ↥H
-- Mathlib.Combinatorics.Additive.SubsetSum
Finset.vadd_finset_subsetSum_subset_subsetSum_insert : ∀ {M : Type u_1} [inst : DecidableEq M] [inst_1 : AddCommMonoid M] {A : Finset M} {a : M},
  a ∉ A → a +ᵥ A.subsetSum ⊆ (insert a A).subsetSum
-- Lean.Attributes
Lean.throwAttrDeclNotOfExpectedType : {m : Type → Type} → [Monad m] → [Lean.MonadError m] → {α : Type} → Lean.Name → Lean.Name → Lean.Expr → Lean.Expr → m α
-- Mathlib.Algebra.Group.Opposite
AddOpposite.instAddMonoid.eq_1 : ∀ {α : Type u_1} [inst : AddMonoid α],
  AddOpposite.instAddMonoid =
    { toAddSemigroup := AddOpposite.instAddSemigroup, toZero := AddOpposite.instAddZeroClass.toZero, zero_add := ⋯,
      add_zero := ⋯, nsmul := fun n a => AddOpposite.op (n • AddOpposite.unop a), nsmul_zero := ⋯, nsmul_succ := ⋯ }
-- Mathlib.CategoryTheory.Action.Concrete
Action.ofMulAction_ρ : ∀ (G : Type u_1) (H : Type u) [inst : Monoid G] [inst_1 : MulAction G H],
  (Action.ofMulAction G H).ρ = (TypeCat.endEquiv H).toMonoidHom.comp MulAction.toEndHom
-- Mathlib.Algebra.Order.GroupWithZero.Basic
PosMulReflectLT.toPosMulReflectLE : ∀ {α : Type u_1} [inst : MonoidWithZero α] [inst_1 : PartialOrder α] [IsLeftCancelMulZero α] [PosMulReflectLT α],
  PosMulReflectLE α
-- Std.Data.Iterators.Lemmas.Equivalence.HetT
Std.Iterators.HetT.prun_pmap : ∀ {m : Type w → Type w'} {α : Type u} {β : Type v} {γ : Type w} [inst : Monad m] [LawfulMonad m]
  {x : Std.Iterators.HetT m α} {f : (a : α) → x.Property a → β} {g : (b : β) → (x.pmap f).Property b → m γ},
  (x.pmap f).prun g = x.prun fun a ha => g (f a ha) ⋯
-- Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Basic
/-- When `C` is monoidal closed and has suitable limits,
then for any `F : J ⥤ C`, `tensorLeft F` has a right adjoint.  -/
CategoryTheory.MonoidalClosed.FunctorCategory.closed : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.MonoidalClosed C] →
        {J : Type u₂} →
          [inst_3 : CategoryTheory.Category.{v₂, u₂} J] →
            [∀ (F₁ F₂ : CategoryTheory.Functor J C),
                  CategoryTheory.Enriched.FunctorCategory.HasFunctorEnrichedHom C F₁ F₂] →
              [∀ (F₁ F₂ : CategoryTheory.Functor J C), CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom C F₁ F₂] →
                (F : CategoryTheory.Functor J C) → CategoryTheory.Closed F
-- Mathlib.Tactic.Linter.TextBased
_private.Mathlib.Tactic.Linter.TextBased.0.Mathlib.Linter.TextBased.ComparisonResult.Comparable.sizeOf_spec : sizeOf Mathlib.Linter.TextBased.ComparisonResult.Comparable✝ = 1
-- Mathlib.Topology.Irreducible
IrreducibleSpace.toPreirreducibleSpace : ∀ {X : Type u_3} {inst : TopologicalSpace X} [self : IrreducibleSpace X], PreirreducibleSpace X
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithTop.map_one : ∀ {α : Type u} [inst : One α] {β : Type u_1} (f : α → β), WithTop.map f 1 = ↑(f 1)
-- Mathlib.NumberTheory.Padics.AddChar
PadicInt.continuousAddCharEquiv_apply : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {R : Type u_1} [inst_1 : NormedRing R] [inst_2 : Algebra ℤ_[p] R]
  [inst_3 : IsBoundedSMul ℤ_[p] R] [inst_4 : IsUltrametricDist R] [inst_5 : CompleteSpace R] {κ : AddChar ℤ_[p] R}
  (hκ : Continuous ⇑κ), ↑((PadicInt.continuousAddCharEquiv p R) ⟨κ, hκ⟩) = κ 1 - 1
-- Mathlib.Order.PropInstances
inf_Prop_eq : (fun x1 x2 => min x1 x2) = fun x1 x2 => x1 ∧ x2
-- Mathlib.Order.CompleteLattice.Lemmas
iInf_sup_iInf_le : ∀ {α : Type u_1} {ι : Sort u_4} [inst : CompleteLattice α] (f g : ι → α), (⨅ i, f i) ⊔ ⨅ i, g i ≤ ⨅ i, f i ⊔ g i
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.mk.inj : ∀ {Functions : ℕ → Type u} {Relations : ℕ → Type v} {Functions_1 : ℕ → Type u} {Relations_1 : ℕ → Type v},
  { Functions := Functions, Relations := Relations } = { Functions := Functions_1, Relations := Relations_1 } →
    Functions = Functions_1 ∧ Relations = Relations_1
-- Mathlib.ModelTheory.Semantics
/-- **Alias** of `FirstOrder.Language.LHom.setOfPred_realize_onFormula`. -/
FirstOrder.Language.LHom.setOf_realize_onFormula : ∀ {L : FirstOrder.Language} {L' : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'}
  [inst_1 : L'.Structure M] (φ : L →ᴸ L') [φ.IsExpansionOn M] (ψ : L.Formula α),
  Set.ofPred (φ.onFormula ψ).Realize = Set.ofPred ψ.Realize
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.forall : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] {P : MonoidAlgebra R M → Prop},
  (∀ (p : MonoidAlgebra R M), P p) ↔ ∀ (q : M →₀ R), P (MonoidAlgebra.ofCoeff q)
-- Init.Data.Sum.Lemmas
Sum.inr.inj_iff : ∀ {α : Type u_1} {β : Type u_2} {a b : β}, Sum.inr a = Sum.inr b ↔ a = b
-- Mathlib.Order.CompleteLattice.Basic
Prod.swap_iInf : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [inst : InfSet α] [inst_1 : InfSet β] (f : ι → α × β),
  (iInf f).swap = ⨅ i, (f i).swap
-- Mathlib.Data.Seq.Computation
Computation.bind_pure' : ∀ {α : Type u} (s : Computation α), s.bind Computation.pure = s
-- Mathlib.Analysis.Asymptotics.Theta
Asymptotics.IsTheta.isBigO_congr_right : ∀ {α : Type u_1} {E : Type u_3} {F' : Type u_7} {G' : Type u_8} [inst : Norm E] [inst_1 : SeminormedAddCommGroup F']
  [inst_2 : SeminormedAddCommGroup G'] {f : α → E} {g' : α → F'} {k' : α → G'} {l : Filter α},
  g' =Θ[l] k' → (f =O[l] g' ↔ f =O[l] k')
-- Lean.Server.Snapshots
Lean.Server.Snapshots.Snapshot.mk.sizeOf_spec : ∀ (stx : Lean.Syntax) (mpState : Lean.Parser.ModuleParserState) (cmdState : Lean.Elab.Command.State),
  sizeOf { stx := stx, mpState := mpState, cmdState := cmdState } = 1 + sizeOf stx + sizeOf mpState + sizeOf cmdState
-- Mathlib.Analysis.SpecialFunctions.Log.Base
Real.logb_lt_iff_lt_rpow : ∀ {b x y : ℝ}, 1 < b → 0 < x → (Real.logb b x < y ↔ x < b ^ y)
-- Mathlib.Analysis.Normed.MulAction
nnnorm_smul : ∀ {α : Type u_1} {β : Type u_2} [inst : SeminormedRing α] [inst_1 : SeminormedAddGroup β] [inst_2 : SMul α β]
  [NormSMulClass α β] (r : α) (x : β), ‖r • x‖₊ = ‖r‖₊ * ‖x‖₊
-- Mathlib.Analysis.Normed.Lp.LpEquiv
coe_lpBCFₗᵢ : ∀ {α : Type u_1} {E : Type u_2} {𝕜 : Type u_5} [inst : TopologicalSpace α] [inst_1 : DiscreteTopology α]
  [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace 𝕜 E]
  (f : ↥(lp (fun x => E) ⊤)), ⇑((lpBCFₗᵢ E 𝕜) f) = ↑f
-- Lean.Meta.MethodSpecs
_private.Lean.Meta.MethodSpecs.0.Lean.MethodSpecsInfo.mk.inj : ∀ {clsName : Lean.Name} {privateSpecs : Bool} {fieldImpls : Array (Lean.Name × Lean.Name)}
  {thms : Array Lean.MethodSpecTheorem✝} {clsName_1 : Lean.Name} {privateSpecs_1 : Bool}
  {fieldImpls_1 : Array (Lean.Name × Lean.Name)} {thms_1 : Array Lean.MethodSpecTheorem✝},
  { clsName := clsName, privateSpecs := privateSpecs, fieldImpls := fieldImpls, thms := thms } =
      { clsName := clsName_1, privateSpecs := privateSpecs_1, fieldImpls := fieldImpls_1, thms := thms_1 } →
    clsName = clsName_1 ∧ privateSpecs = privateSpecs_1 ∧ fieldImpls = fieldImpls_1 ∧ thms = thms_1
-- Init.Data.Rat.Lemmas
Rat.mul_one : ∀ (a : ℚ), a * 1 = a
-- Init.Data.Vector.Lemmas
Vector.flatMap_empty : ∀ {α : Type u_1} {β : Type u_2} {m : ℕ} {f : α → Vector β m}, #v[].flatMap f = Vector.cast ⋯ #v[]
-- Init.Data.BitVec.Lemmas
BitVec.extractLsb'_or : ∀ {w : ℕ} {x y : BitVec w} {start len : ℕ},
  BitVec.extractLsb' start len (x ||| y) = BitVec.extractLsb' start len x ||| BitVec.extractLsb' start len y
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
WeierstrassCurve.Jacobian.Point.toAffine_zero : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Jacobian F},
  WeierstrassCurve.Jacobian.Point.toAffine W ![1, 1, 0] = 0
-- Mathlib.Data.Finset.Lattice.Fold
Finset.sup_himp_right : ∀ {α : Type u_2} {ι : Type u_5} [inst : BooleanAlgebra α] {s : Finset ι},
  s.Nonempty → ∀ (f : ι → α) (a : α), (s.sup fun b => f b ⇨ a) = s.inf f ⇨ a
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.Spanning.isBase_restrict_iff : ∀ {α : Type u_2} {M : Matroid α} {S B : Set α}, M.Spanning S → ((M.restrict S).IsBase B ↔ M.IsBase B ∧ B ⊆ S)
-- Init.Data.Int.LemmasAux
Int.ble'_eq_true : ∀ (a b : ℤ), (a.ble' b = true) = (a ≤ b)
-- Lean.Meta.ACLt
_private.Lean.Meta.ACLt.0.Lean.Meta.ACLt.main.lexSameCtor : Lean.Meta.ACLt.ReduceMode → Lean.Expr → Lean.Expr → Lean.MetaM Bool
-- Init.Data.Int.DivMod.Lemmas
Int.ediv_lt_self_of_pos_of_ne_one : ∀ {x y : ℤ}, 0 < x → y ≠ 1 → x / y < x
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect
Std.IterM.toList_ensureTermination_eq_match_step : ∀ {α β : Type w} {m : Type w → Type w'} [inst : Monad m] [LawfulMonad m] [inst_2 : Std.Iterator α m β]
  [inst_3 : Std.Iterators.Finite α m] {it : Std.IterM m β},
  it.ensureTermination.toList = do
    let __do_lift ← it.step
    match ↑__do_lift.inflate with
      | Std.IterStep.yield it' out => do
        let __do_lift ← it'.toList
        pure (out :: __do_lift)
      | Std.IterStep.skip it' => it'.toList
      | Std.IterStep.done => pure []
-- Mathlib.Algebra.Order.Group.Action
smul_iInf_le : ∀ {ι : Sort u_1} {M : Type u_2} {α : Type u_3} [inst : SMul M α] [inst_1 : CompleteLattice α]
  [CovariantClass M α HSMul.hSMul LE.le] {m : M} {t : ι → α}, m • iInf t ≤ ⨅ i, m • t i
-- Mathlib.LinearAlgebra.TensorPower.Basic
TensorPower.cast_tprod : ∀ (R : Type u_1) (M : Type u_2) [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {i j : ℕ}
  (h : i = j) (a : Fin i → M),
  (TensorPower.cast R M h) ((PiTensorProduct.tprod R) a) = (PiTensorProduct.tprod R) (a ∘ Fin.cast ⋯)
-- Lean.Meta.Tactic.Grind.AC.Util
Lean.Meta.Grind.AC.isIdempotent : Lean.Meta.Grind.AC.ACM Bool
-- Mathlib.Topology.Compactness.Compact
/-- A relative version of `IsCompact.nhdsSet_prod_eq`: if `s` and `t` are compact sets,
then the neighborhoods filter of `s ×ˢ t` within `s' ×ˢ t'` is the product of the neighborhoods
filters of `s` and `t` within `s'` and `t'`.

For general sets, only the `≤` inequality holds, see `nhdsSetWithin_prod_le`.  -/
IsCompact.nhdsSetWithin_prod_eq : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {s s' : Set X} {t t' : Set Y},
  IsCompact s → IsCompact t → nhdsSetWithin (s ×ˢ t) (s' ×ˢ t') = nhdsSetWithin s s' ×ˢ nhdsSetWithin t t'
-- Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic
/-- A normal epimorphism is a morphism which is the cokernel of some morphism.  -/
CategoryTheory.NormalEpi.g : {C : Type u₁} →
  {inst : CategoryTheory.Category.{v₁, u₁} C} →
    {X Y : C} →
      {inst_1 : CategoryTheory.Limits.HasZeroMorphisms C} →
        {f : X ⟶ Y} → [self : CategoryTheory.NormalEpi f] → CategoryTheory.NormalEpi.W f ⟶ X
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.OplaxMonoidal.δ_natural_left : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C} {D : Type u₂}
  {inst_2 : CategoryTheory.Category.{v₂, u₂} D} {inst_3 : CategoryTheory.MonoidalCategory D}
  (F : CategoryTheory.Functor C D) [self : F.OplaxMonoidal] {X Y : C} (f : X ⟶ Y) (X' : C),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.δ F X X')
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (F.map f) (F.obj X')) =
    CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.MonoidalCategoryStruct.whiskerRight f X'))
      (CategoryTheory.Functor.OplaxMonoidal.δ F Y X')
-- Mathlib.CategoryTheory.Preadditive.Biproducts
/-- In a preadditive category, we can construct a binary biproduct for `X Y : C` from
any binary bicone `b` satisfying `total : b.fst ≫ b.inl + b.snd ≫ b.inr = 𝟙 b.X`.

(That is, such a bicone is a limit cone and a colimit cocone.)
 -/
CategoryTheory.Limits.isBinaryBilimitOfTotal : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {X Y : C} →
        (b : CategoryTheory.Limits.BinaryBicone X Y) →
          CategoryTheory.CategoryStruct.comp b.fst b.inl + CategoryTheory.CategoryStruct.comp b.snd b.inr =
              CategoryTheory.CategoryStruct.id b.pt →
            b.IsBilimit
-- Mathlib.Data.NNReal.Defs
NNReal.lt_inv_iff_mul_lt : ∀ {r p : NNReal}, p ≠ 0 → (r < p⁻¹ ↔ r * p < 1)
-- Mathlib.GroupTheory.Coprod.Basic
AddMonoid.Coprod.mrange_lift : ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] [inst_2 : AddMonoid P]
  (f : M →+ P) (g : N →+ P),
  AddMonoidHom.mrange (AddMonoid.Coprod.lift f g) = AddMonoidHom.mrange f ⊔ AddMonoidHom.mrange g
-- Mathlib.SetTheory.Ordinal.Basic
/-- A variation on `Cardinal.lt_ord` using `≤`: If `o` is no greater than the
initial ordinal of cardinality `c`, then its cardinal is no greater than `c`.

The converse, however, is false (for instance, `o = ω+1` and `c = ℵ₀`).
 -/
Cardinal.card_le_of_le_ord : ∀ {o : Ordinal.{u_1}} {c : Cardinal.{u_1}}, o ≤ c.ord → o.card ≤ c
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.BinaryCofan.mk_inl : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y P : C} (ι₁ : X ⟶ P) (ι₂ : Y ⟶ P),
  (CategoryTheory.Limits.BinaryCofan.mk ι₁ ι₂).inl = ι₁
-- Mathlib.Topology.Sequences
CompactSpace.tendsto_subseq : ∀ {X : Type u_1} [inst : TopologicalSpace X] [FirstCountableTopology X] [CompactSpace X] (x : ℕ → X),
  ∃ a φ, StrictMono φ ∧ Filter.Tendsto (x ∘ φ) Filter.atTop (nhds a)
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
/-- This functor `SimplexCategory ⥤ Cat` sends `⦋n⦌` (for `n : ℕ`)
to the category attached to the ordered set `{0, 1, ..., n}`  -/
SimplexCategory.toCat : CategoryTheory.Functor SimplexCategory CategoryTheory.Cat
-- Mathlib.GroupTheory.GroupAction.Basic
Module.stabilizer_units_eq_bot_of_ne_zero : ∀ (R : Type u_1) {M : Type u_2} [inst : Ring R] [IsDomain R] [inst_2 : AddCommGroup M] [inst_3 : Module R M]
  [Module.IsTorsionFree R M] {x : M}, x ≠ 0 → MulAction.stabilizer Rˣ x = ⊥
-- Mathlib.Algebra.Order.Hom.Monoid
OrderAddMonoidIso.refl_trans : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Add α] [inst_3 : Add β]
  (f : α ≃+o β), (OrderAddMonoidIso.refl α).trans f = f
-- Std.Data.TreeSet.Raw.Basic
/-- Internal implementation detail of the tree set.  -/
Std.TreeSet.Raw.inner : {α : Type u} →
  {cmp : autoParam (α → α → Ordering) Std.TreeSet.Raw._auto_1} → Std.TreeSet.Raw α cmp → Std.TreeMap.Raw α Unit cmp
-- Mathlib.RingTheory.IsAdjoinRoot
IsAdjoinRoot.mkOfAdjoinEqTop_map : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [inst_3 : IsDomain R]
  [inst_4 : IsDomain S] [inst_5 : Module.IsTorsionFree R S] [inst_6 : IsIntegrallyClosed R] {α : S}
  (hα : IsIntegral R α) (hα₂ : R[α] = ⊤), (IsAdjoinRoot.mkOfAdjoinEqTop hα hα₂).map = Polynomial.aeval α
-- Mathlib.RingTheory.Coprime.Basic
IsCoprime.sub_mul_left_right_iff : ∀ {R : Type u} [inst : CommRing R] {x y z : R}, IsCoprime x (y - x * z) ↔ IsCoprime x y
-- Init.Data.Fin.Fold
Fin.foldrM_add : ∀ {m : Type u_1 → Type u_2} {n k : ℕ} {α : Type u_1} [inst : Monad m] [LawfulMonad m] (f : Fin (n + k) → α → m α),
  Fin.foldrM (n + k) f = fun x =>
    Fin.foldrM k (fun i => f (Fin.natAdd n i)) x >>= Fin.foldrM n fun i => f (Fin.castLE ⋯ i)
-- Lean.DocString.Parser
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.code.codeContentsFn : ℕ → Lean.Parser.ParserFn
-- Mathlib.Combinatorics.Enumerative.Composition
List.map_length_splitWrtCompositionAux : ∀ {α : Type u_1} {ns : List ℕ} {l : List α}, ns.sum ≤ l.length → List.map List.length (l.splitWrtCompositionAux ns) = ns
-- Mathlib.Algebra.Group.Subgroup.Ker
MonoidHom.ker_id : ∀ {G : Type u_1} [inst : Group G], (MonoidHom.id G).ker = ⊥
-- Mathlib.Analysis.Normed.Group.Seminorm
AddGroupNorm.instIsAddApplyReal : ∀ {E : Type u_3} [inst : AddGroup E], IsAddApply (AddGroupNorm E) E ℝ
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
MeasurableEquiv.symm_refl : ∀ (α : Type u_6) [inst : MeasurableSpace α], (MeasurableEquiv.refl α).symm = MeasurableEquiv.refl α
-- Mathlib.Analysis.Asymptotics.Lemmas
Asymptotics.isBigO_nat_atTop_iff : ∀ {E'' : Type u_9} {F'' : Type u_10} [inst : NormedAddCommGroup E''] [inst_1 : NormedAddCommGroup F''] {f : ℕ → E''}
  {g : ℕ → F''}, (∀ (x : ℕ), g x = 0 → f x = 0) → (f =O[Filter.atTop] g ↔ ∃ C, ∀ (x : ℕ), ‖f x‖ ≤ C * ‖g x‖)
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.toVal_sub : ∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] [inst_1 : Ring R] (v : Valuation R Γ₀)
  (x y : R), WithVal.toVal v (x - y) = WithVal.toVal v x - WithVal.toVal v y
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.Rel.below.whisker_right : ∀ {B : Type u} [inst : Quiver B]
  {motive :
    {a b : CategoryTheory.FreeBicategory B} →
      {f g : a ⟶ b} →
        (a_1 a_2 : CategoryTheory.FreeBicategory.Hom₂ f g) → CategoryTheory.FreeBicategory.Rel a_1 a_2 → Prop}
  {a b c : B} (f g : CategoryTheory.FreeBicategory.Hom a b) (h : CategoryTheory.FreeBicategory.Hom b c)
  (η η' : CategoryTheory.FreeBicategory.Hom₂ f g) (a_1 : CategoryTheory.FreeBicategory.Rel η η'),
  CategoryTheory.FreeBicategory.Rel.below a_1 → motive η η' a_1 → CategoryTheory.FreeBicategory.Rel.below ⋯
-- Mathlib.Geometry.Manifold.LocalDiffeomorph
/-- `f : M → N` is called a **`C^n` local diffeomorphism at `x`** iff there exist
open sets `U ∋ x` and `V ∋ f x` and a diffeomorphism `Φ : U → V` such that `f = Φ` on `U`.  -/
IsLocalDiffeomorphAt : {𝕜 : 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] →
                {H₁ : Type u_5} →
                  [inst_5 : TopologicalSpace H₁] →
                    {H₂ : Type u_6} →
                      [inst_6 : TopologicalSpace H₂] →
                        ModelWithCorners 𝕜 E H₁ →
                          ModelWithCorners 𝕜 F H₂ →
                            {M : Type u_8} →
                              [inst : TopologicalSpace M] →
                                [ChartedSpace H₁ M] →
                                  {N : Type u_9} →
                                    [inst : TopologicalSpace N] → [ChartedSpace H₂ N] → WithTop ℕ∞ → (M → N) → M → Prop
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.yonedaEquiv_symm_naturality_left_assoc : ∀ {X : SSet} {m n : SimplexCategory} (f : m ⟶ n) (g : X.obj (Opposite.op n)) {Z : SSet} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.map f)
      (CategoryTheory.CategoryStruct.comp (SSet.yonedaEquiv.symm g) h) =
    CategoryTheory.CategoryStruct.comp (SSet.yonedaEquiv.symm ((CategoryTheory.ConcreteCategory.hom (X.map f.op)) g)) h
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.HomologyData.ofIso_right_p : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (e : S₁ ≅ S₂) (h : S₁.HomologyData),
  (CategoryTheory.ShortComplex.HomologyData.ofIso e h).right.p =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.inv e.hom.τ₂) h.right.p
-- Mathlib.RingTheory.Algebraic.Integral
IsAlgebraic.nsmul : ∀ {R : Type u_1} {A : Type u_3} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] {a : A},
  IsAlgebraic R a → ∀ (n : ℕ), IsAlgebraic R (n • a)
-- Mathlib.AlgebraicTopology.SimplicialSet.SubcomplexColimits
/-- Abbreviation for bicartesian squares in the lattice of subcomplexes of a simplicial set.  -/
SSet.Subcomplex.BicartSq : {X : SSet} → X.Subcomplex → X.Subcomplex → X.Subcomplex → X.Subcomplex → Prop
-- Mathlib.GroupTheory.GroupAction.SubMulAction
/-- Embedding of a submodule `p` to the ambient space `M`.  -/
SubMulAction.subtype : {R : Type u} → {M : Type v} → [inst : SMul R M] → (p : SubMulAction R M) → ↥p →ₑ[id] M
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVExpr.eval.eq_5 : ∀ {w : ℕ} (assign : Std.Tactic.BVDecide.BVExpr.Assignment) (op : Std.Tactic.BVDecide.BVUnOp)
  (operand : Std.Tactic.BVDecide.BVExpr w),
  Std.Tactic.BVDecide.BVExpr.eval assign (Std.Tactic.BVDecide.BVExpr.un op operand) =
    op.eval (Std.Tactic.BVDecide.BVExpr.eval assign operand)