mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Real.continuous_mul_log : Continuous fun x => x * Real.log x
-- Mathlib.Data.ENNReal.Inv
ENNReal.div_eq_inv_mul : ∀ {a b : ENNReal}, a / b = b⁻¹ * a
-- Mathlib.LinearAlgebra.Determinant
Module.Basis.det_reindex_symm : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {ι : Type u_4}
  [inst_3 : DecidableEq ι] [inst_4 : Fintype ι] {ι' : Type u_6} [inst_5 : Fintype ι'] [inst_6 : DecidableEq ι']
  (b : Module.Basis ι R M) (v : ι → M) (e : ι' ≃ ι), (b.reindex e.symm).det (v ∘ ⇑e) = b.det v
-- Lean.Meta.Tactic.Util
/-- Check if a goal is of a subsingleton type.  -/
Lean.MVarId.isSubsingleton : Lean.MVarId → Lean.MetaM Bool
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
BoundedContinuousFunction.coe_ofNat : ∀ {α : Type u} [inst : TopologicalSpace α] {R : Type u_1} [inst_1 : SeminormedRing R] (n : ℕ) [inst_2 : n.AtLeastTwo],
  ⇑(OfNat.ofNat n) = OfNat.ofNat n
-- Mathlib.Data.Seq.Defs
Stream'.Seq.nil_ne_cons : ∀ {α : Type u} {x : α} {s : Stream'.Seq α}, Stream'.Seq.nil ≠ Stream'.Seq.cons x s
-- Lean.Meta.Tactic.Simp.Main
_private.Lean.Meta.Tactic.Simp.Main.0.Lean.Meta.Simp.lambdaTelescopeDSimp.go : {α : Type} → (Array Lean.Expr → Lean.Expr → Lean.Meta.SimpM α) → Array Lean.Expr → Lean.Expr → Lean.Meta.SimpM α
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.homologyMap'_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (h₁ : S₁.HomologyData) (h₂ : S₂.HomologyData),
  CategoryTheory.ShortComplex.homologyMap' 0 h₁ h₂ = 0
-- Lean.Data.Options
Lean.Option.mk.inj : ∀ {α : Type} {name : Lean.Name} {defValue : α} {name_1 : Lean.Name} {defValue_1 : α},
  { name := name, defValue := defValue } = { name := name_1, defValue := defValue_1 } →
    name = name_1 ∧ defValue = defValue_1
-- Mathlib.Analysis.Normed.Lp.ProdLp
WithLp.prod_nnnorm_eq_of_L1 : ∀ {α : Type u_2} {β : Type u_3} [inst : SeminormedAddCommGroup α] [inst_1 : SeminormedAddCommGroup β]
  (x : WithLp 1 (α × β)), ‖x‖₊ = ‖x.fst‖₊ + ‖x.snd‖₊
-- Mathlib.Order.ModularLattice
/-- The diamond isomorphism between the closed intervals `[a ⊓ b, b]` and `[a, a ⊔ b]`  -/
infIccOrderIsoIccSup' : {α : Type u_1} → [inst : Lattice α] → [IsModularLattice α] → (a b : α) → ↑(Set.Icc (a ⊓ b) b) ≃o ↑(Set.Icc a (a ⊔ b))
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.equivHomsetRightOfNatIso.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F F' : CategoryTheory.Functor C D} (iso : F ≅ F') {X : C} {Y : D},
  CategoryTheory.Adjunction.equivHomsetRightOfNatIso iso =
    { toFun := fun f => CategoryTheory.CategoryStruct.comp f (iso.hom.app X),
      invFun := fun g => CategoryTheory.CategoryStruct.comp g (iso.inv.app X), left_inv := ⋯, right_inv := ⋯ }
-- Init.Data.Float.Model.Float
/-- Converts a `Float.Model` to an `Int16`, truncating after the decimal point, sending `NaN` to
`0` and clamping out-of-range values and infinities.
 -/
Float.Model.toInt16 : Float.Model → Int16
-- Mathlib.Probability.CondVar
/-- Conditional variance of a real-valued random variable. It is defined as `0` if any one of the
following conditions is true:
- `m` is not a sub-σ-algebra of `m₀`,
- `μ` is not σ-finite with respect to `m`,
- `X - μ[X | m]` is not square-integrable.  -/
ProbabilityTheory.«termVar[_;_|_]» : Lean.ParserDescr
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.map_injective_of_injective : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_4}
  [inst_2 : FunLike F M N] [mc : AddMonoidHomClass F M N] {f : F},
  Function.Injective ⇑f → Function.Injective (AddSubmonoid.map f)
-- Mathlib.Order.Interval.Set.OrdConnected
Set.ordConnected_uIoc : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, (Set.uIoc a b).OrdConnected
-- Mathlib.Tactic.Abel
Mathlib.Tactic.Abel.smulg.eq_1 : ∀ {α : Type u_1} [inst : AddCommGroup α] (n : ℤ) (x : α), Mathlib.Tactic.Abel.smulg n x = n • x
-- Mathlib.Analysis.Calculus.Deriv.Mul
deriv_const_mul_id' : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] (c : 𝕜), (deriv fun x => c * x) = fun x => c
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKeyD_eq_fallback : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {a fallback : α}, a ∉ m → m.getKeyD a fallback = fallback
-- Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
QuasispectrumRestricts.of_subset_range_algebraMap : ∀ {R : Type u_3} {S : Type u_4} {A : Type u_5} [inst : Semifield R] [inst_1 : Field S] [inst_2 : NonUnitalRing A]
  [inst_3 : Module R A] [inst_4 : Module S A] [inst_5 : Algebra R S] {a : A} {f : S → R},
  Function.LeftInverse f ⇑(algebraMap R S) →
    quasispectrum S a ⊆ Set.range ⇑(algebraMap R S) → QuasispectrumRestricts a f
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.dblY.eq_1 : ∀ {R : Type r} [inst : CommRing R] (W' : WeierstrassCurve.Projective R) (P : Fin 3 → R),
  W'.dblY P = W'.negY ![W'.dblX P, W'.negDblY P, W'.dblZ P]
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.inv_hom_s₁_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E F : CategoryTheory.PreOneHypercover S} (e : E ≅ F)
  {i j : F.I₀} (k : F.I₁ i j), e.hom.s₁ (e.inv.s₁ k) = (CategoryTheory.PreOneHypercover.congrIndexOneOfEq ⋯ ⋯) k
-- Mathlib.Probability.ProbabilityMassFunction.Constructions
/-- The functorial action of a function on a `PMF`.  -/
PMF.map : {α : Type u_1} → {β : Type u_2} → (α → β) → PMF α → PMF β
-- Init.MetaTypes
/-- If true (default: false), eliminate unused lets rather than extract them.  -/
Lean.Meta.ExtractLetsConfig.usedOnly : Lean.Meta.ExtractLetsConfig → Bool
-- Mathlib.Probability.Independence.Kernel.IndepFun
ProbabilityTheory.Kernel.iIndepFun.meas_biInter : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {β : ι → Type u_8} {mβ : (i : ι) → MeasurableSpace (β i)}
  {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α}
  {s : ι → Set Ω} {S : Finset ι} {f : (x : ι) → Ω → β x},
  ProbabilityTheory.Kernel.iIndepFun f κ μ →
    (∀ i ∈ S, MeasurableSet (s i)) → ∀ᵐ (a : α) ∂μ, (κ a) (⋂ i ∈ S, s i) = ∏ i ∈ S, (κ a) (s i)
-- Mathlib.LinearAlgebra.Trace
LinearMap.trace_comp_eq_mul_of_commute_of_isNilpotent : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsReduced R]
  {f g : Module.End R M} (μ : R),
  Commute f g →
    IsNilpotent (g - (algebraMap R (Module.End R M)) μ) → (LinearMap.trace R M) (f ∘ₗ g) = μ * (LinearMap.trace R M) f
-- Std.Data.ExtTreeMap.Basic
Std.ExtTreeMap.mk : {α : Type u} →
  {β : Type v} →
    {cmp : autoParam (α → α → Ordering) Std.ExtTreeMap._auto_1} →
      Std.ExtDTreeMap α (fun x => β) cmp → Std.ExtTreeMap α β cmp
-- Init.Data.Nat.Div.Basic
Nat.mul_div_right : ∀ (n : ℕ) {m : ℕ}, 0 < m → m * n / m = n
-- Mathlib.Algebra.Order.Ring.Unbundled.Rat
Rat.mkRat_pos_iff : ∀ (a : ℤ) {b : ℕ}, b ≠ 0 → (0 < mkRat a b ↔ 0 < a)
-- Mathlib.CategoryTheory.Adjunction.Reflective
CategoryTheory.mem_essImage_of_counit_isSplitEpi : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {j : CategoryTheory.Functor C D} [inst_2 : CategoryTheory.Coreflective j] {A : D}
  [CategoryTheory.IsSplitEpi ((CategoryTheory.coreflectorAdjunction j).counit.app A)], j.essImage A
-- Mathlib.Topology.MetricSpace.BundledFun
PseudoMetric.coe_bot : ∀ {X : Type u_1} {R : Type u_2} [inst : AddZeroClass R] [inst_1 : Preorder R], ⇑⊥ = 0
-- Mathlib.Tactic.NormNum.BigOperators
Mathlib.Meta.Finset.range_zero' : ∀ {n : ℕ}, Mathlib.Meta.NormNum.IsNat n 0 → Finset.range n = ∅
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Order
measurableSet_Ici : ∀ {α : Type u_1} [inst : TopologicalSpace α] {mα : MeasurableSpace α} [OpensMeasurableSpace α] [inst_2 : Preorder α]
  {a : α} [ClosedIciTopology α], MeasurableSet (Set.Ici a)
-- Init.Data.Slice.Array.Iterator
SubarrayIterator.mk : {α : Type u} → Subarray α → SubarrayIterator α
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
AffineSubspace.affineSpan_pair_parallel_iff_exists_unit_smul : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] [IsDomain k] [Module.IsTorsionFree k V] {p₁ q₁ p₂ q₂ : P},
  line[k, p₁, q₁].Parallel line[k, p₂, q₂] ↔ ∃ z, z • (q₂ -ᵥ p₂) = q₁ -ᵥ p₁
-- Mathlib.Algebra.Category.Grp.Limits
/-- If `(F ⋙ forget AddGrpCat).sections` is `u`-small, `F` has a limit.  -/
AddGrpCat.hasLimit : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddGrpCat)
  [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget AddGrpCat)).sections], CategoryTheory.Limits.HasLimit F
-- Mathlib.Order.Antisymmetrization
AntisymmRel.le_congr_left : ∀ {α : Type u_1} {a b c : α} [inst : Preorder α], AntisymmRel (fun x1 x2 => x1 ≤ x2) a b → (a ≤ c ↔ b ≤ c)
-- Mathlib.Data.Fin.Tuple.Basic
Fin.forall_fin_zero_pi : ∀ {α : Fin 0 → Sort u_1} {P : ((i : Fin 0) → α i) → Prop}, (∀ (x : (i : Fin 0) → α i), P x) ↔ P finZeroElim
-- Mathlib.Analysis.BoxIntegral.Partition.Split
BoxIntegral.Prepartition.inf_splitMany : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) (s : Finset (ι × ℝ)),
  π ⊓ BoxIntegral.Prepartition.splitMany I s = π.biUnion fun J => BoxIntegral.Prepartition.splitMany J s
-- Mathlib.RingTheory.Ideal.Maps
Submodule.annihilator_eq_top_iff : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {N : Submodule R M}, N.annihilator = ⊤ ↔ N = ⊥
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.addY.eq_1 : ∀ {R : Type r} [inst : CommRing R] (W' : WeierstrassCurve.Jacobian R) (P Q : Fin 3 → R),
  W'.addY P Q = W'.negY ![W'.addX P Q, W'.negAddY P Q, WeierstrassCurve.Jacobian.addZ P Q]
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getD_diff_of_contains_right : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] (h₁ : m₁.WF),
  m₂.WF →
    ∀ {k : α} {fallback : β k},
      Std.DTreeMap.Internal.Impl.contains k m₂ = true → (m₁.diff m₂ ⋯).getD k fallback = fallback
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Normal
CategoryTheory.IsMonHom.Normal.mono : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {inst_1 : CategoryTheory.CartesianMonoidalCategory C}
  {G H : C} {inst_2 : CategoryTheory.GrpObj G} {inst_3 : CategoryTheory.GrpObj H} {φ : H ⟶ G}
  [self : CategoryTheory.IsMonHom.Normal φ], CategoryTheory.Mono φ
-- Mathlib.Order.Partition.Finpartition
Finpartition.avoid_parts_val : ∀ {α : Type u_1} [inst : GeneralizedBooleanAlgebra α] [inst_1 : DecidableEq α] {a : α} (P : Finpartition a) (b : α),
  (P.avoid b).parts.val = (Multiset.map (fun x => x \ b) P.parts.val).dedup.erase ⊥
-- Init.Data.String.FindPos
/-- Obtains the largest valid position that is less than or equal to the given byte position.
 -/
String.Slice.posLE : (s : String.Slice) → String.Pos.Raw → s.Pos
-- Mathlib.Topology.Algebra.ContinuousAffineMap
/-- Applying a `ContinuousAffineMap` commutes with `ContinuousAffineMap.lineMap`.  -/
ContinuousAffineMap.apply_lineMap' : ∀ {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} {Q : Type u_5} [inst : Ring R] [inst_1 : AddCommGroup V]
  [inst_2 : Module R V] [inst_3 : TopologicalSpace P] [inst_4 : AddTorsor V P] [inst_5 : AddCommGroup W]
  [inst_6 : Module R W] [inst_7 : TopologicalSpace Q] [inst_8 : AddTorsor W Q] [inst_9 : TopologicalSpace R]
  [inst_10 : TopologicalSpace V] [inst_11 : TopologicalSpace W] [inst_12 : ContinuousSMul R V]
  [inst_13 : ContinuousSMul R W] [inst_14 : ContinuousVAdd V P] [inst_15 : ContinuousVAdd W Q] (f : P →ᴬ[R] Q)
  (p₀ p₁ : P) (c : R), f ((ContinuousAffineMap.lineMap p₀ p₁) c) = (ContinuousAffineMap.lineMap (f p₀) (f p₁)) c
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.coeff_mul_single_add : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddMonoid M] [IsCancelAdd M] (x : AddMonoidAlgebra R M)
  (r : R) (m m' : M), (x * AddMonoidAlgebra.single m r).coeff (m' + m) = x.coeff m' * r
-- Mathlib.NumberTheory.Pell
/-- If `a` is any solution, then one of `a`, `a⁻¹`, `-a`, `-a⁻¹` has
positive `x` and nonnegative `y`.  -/
Pell.Solution₁.exists_pos_variant : ∀ {d : ℤ}, 0 < d → ∀ (a : Pell.Solution₁ d), ∃ b, 0 < b.x ∧ 0 ≤ b.y ∧ a ∈ {b, b⁻¹, -b, -b⁻¹}
-- Mathlib.Algebra.Homology.ShortComplex.ShortExact
CategoryTheory.ShortComplex.shortExact_iff_of_iso : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (e : S₁ ≅ S₂), S₁.ShortExact ↔ S₂.ShortExact
-- Std.Async.Process
Std.IO.Process.instOrdPId.ord : Std.IO.Process.PId → Std.IO.Process.PId → Ordering
-- Init.Data.Slice.Operations
/-- This type class provides support for the `Slice.size` function.
 -/
Std.Slice.SliceSize : Type u → Type u
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
CategoryTheory.instIsRegularMonoUnopOfIsRegularEpiOpposite : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : Cᵒᵖ} (f : X ⟶ Y) [CategoryTheory.IsRegularEpi f],
  CategoryTheory.IsRegularMono f.unop
-- Mathlib.Order.Category.BoolAlg
BoolAlg.hom_comp : ∀ {X Y Z : BoolAlg} (f : X ⟶ Y) (g : Y ⟶ Z),
  BoolAlg.Hom.hom (CategoryTheory.CategoryStruct.comp f g) = (BoolAlg.Hom.hom g).comp (BoolAlg.Hom.hom f)
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.IsAffineOpen.ideal_le_iff : ∀ {X : AlgebraicGeometry.Scheme} {U : X.Opens},
  AlgebraicGeometry.IsAffineOpen U →
    ∀ {I J : Ideal ↑(X.presheaf.obj (Opposite.op U))},
      I ≤ J ↔
        ∀ (x : ↥X) (h : x ∈ U),
          Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ U x h)) I ≤
            Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ U x h)) J
-- Mathlib.Order.Category.BddLat
BddLat.coe_forget_to_semilatInf : ∀ (X : BddLat), ((CategoryTheory.forget₂ BddLat SemilatInfCat).obj X).X = ↑X.toLat
-- Mathlib.Algebra.Category.Grp.Basic
GrpCat.instInhabited : Inhabited GrpCat
-- Lean.Meta.InferType
/-- `isTypeQuickApp f n` is an "approximate" predicate which returns `LBool.true` if `f` applied to
`n` arguments is a type.
 -/
_private.Lean.Meta.InferType.0.Lean.Meta.isTypeQuickApp : Lean.Expr → ℕ → Lean.MetaM Lean.LBool
-- Mathlib.Algebra.GroupWithZero.Action.Defs
AddMonoid.nat_smulCommClass' : ∀ {M : Type u_12} {A : Type u_13} [inst : AddMonoid A] [inst_1 : DistribSMul M A], SMulCommClass M ℕ A
-- Mathlib.Order.Types.Defs
/-- The instance for some arbitrary linear order on `Type u` , order isomorphic within
order type `o`.  -/
OrderType.instLinearOrderToType : (o : OrderType.{u_1}) → LinearOrder o.ToType
-- Mathlib.Data.Finsupp.Fin
Finsupp.cons_support : ∀ {n : ℕ} {M : Type u_1} [inst : Zero M] {y : M} {s : Fin n →₀ M},
  (Finsupp.cons y s).support ⊆ insert 0 (Finset.map (Fin.succEmb n) s.support)
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.Opens.isoOfLE_inv_ι_assoc : ∀ {X : AlgebraicGeometry.Scheme} {U V : X.Opens} (hUV : U ≤ V) {Z : AlgebraicGeometry.Scheme} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Opens.isoOfLE hUV).inv
      (CategoryTheory.CategoryStruct.comp ((TopologicalSpace.Opens.map V.ι.base).obj U).ι
        (CategoryTheory.CategoryStruct.comp V.ι h)) =
    CategoryTheory.CategoryStruct.comp U.ι h
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.IsStableUnderBaseChange.unop : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty Cᵒᵖ}
  [P.IsStableUnderBaseChange], P.unop.IsStableUnderCobaseChange
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.functorEquiv_inverse_obj_obj_fst : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) (X : Type u₄)
  [inst_3 : CategoryTheory.Category.{v₄, u₄} X] (S : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X)
  (x : X), (((CategoryTheory.Limits.CategoricalPullback.functorEquiv F G X).inverse.obj S).obj x).fst = S.fst.obj x
-- Mathlib.Data.Set.Subsingleton
Set.Nontrivial.mono : ∀ {α : Type u} {s t : Set α}, s.Nontrivial → s ⊆ t → t.Nontrivial
-- Init.Data.UInt.Lemmas
UInt8.ofBitVec_ofNatLT : ∀ {n : ℕ} (hn : n < 2 ^ 8), { toBitVec := n#'hn } = UInt8.ofNatLT n hn
-- Batteries.Recycling.RBTree.Depth
RBTree.RBNode.Balanced.le_size : ∀ {α : Type u_1} {t : RBTree.RBNode α} {c : RBTree.RBColor} {n : ℕ},
  t.Balanced c n → 2 ^ RBTree.RBNode.depthLB c n ≤ t.size + 1
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.preimage_sub_const_Ico : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] (a b c : α),
  (fun x => x - a) ⁻¹' Set.Ico b c = Set.Ico (b + a) (c + a)
-- Lean.Elab.Tactic.Omega.MinNatAbs
Lean.Elab.Tactic.Omega.List.nonzeroMinimum_le : ∀ {a : ℕ} {xs : List ℕ}, a ∈ xs → a ≠ 0 → Lean.Elab.Tactic.Omega.List.nonzeroMinimum xs ≤ a
-- Mathlib.Data.TypeVec
/-- specialized cases distinction for an arrow in the category of 0-length type vectors  -/
TypeVec.typevecCasesNil₂ : {β : TypeVec.Arrow Fin2.elim0 Fin2.elim0 → Sort u_1} →
  β TypeVec.nilFun → (f : TypeVec.Arrow Fin2.elim0 Fin2.elim0) → β f
-- Std.Sat.AIG.RefVecOperator.Zip
Std.Sat.AIG.RefVec.zip_decl_eq : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {len : ℕ} {aig : Std.Sat.AIG α} (input : aig.BinaryRefVec len)
  (func : (aig : Std.Sat.AIG α) → aig.BinaryInput → Std.Sat.AIG.Entrypoint α)
  [inst_2 : Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.BinaryInput func]
  [inst_3 : Std.Sat.AIG.RefVec.LawfulZipOperator α func] (idx : ℕ) (h1 : idx < aig.decls.size)
  (h2 : idx < (Std.Sat.AIG.RefVec.zip aig input func).aig.decls.size),
  (Std.Sat.AIG.RefVec.zip aig input func).aig.decls[idx] = aig.decls[idx]
-- Mathlib.CategoryTheory.Iso
/-- Composition of the two directions of an isomorphism is the identity on the source.  -/
CategoryTheory.Iso.hom_inv_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (self : X ≅ Y),
  CategoryTheory.CategoryStruct.comp self.hom self.inv = CategoryTheory.CategoryStruct.id X
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
/-- In conditionally complete orders with a bottom element, the nonempty condition can be omitted
from `lt_ciSup_iff`.  -/
lt_ciSup_iff' : ∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompleteLinearOrderBot α] {a : α} {f : ι → α},
  BddAbove (Set.range f) → (a < iSup f ↔ ∃ i, a < f i)
-- Mathlib.CategoryTheory.Monoidal.PushoutProduct
CategoryTheory.MonoidalCategory.Arrow.PullbackHom.isInitialIso_inv_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  [inst_2 : CategoryTheory.CartesianMonoidalCategory C] [inst_3 : CategoryTheory.MonoidalClosed C]
  [inst_4 : CategoryTheory.BraidedCategory C] (X : CategoryTheory.Arrow C) {I : C}
  (i : CategoryTheory.Limits.IsInitial I) {W : C},
  (CategoryTheory.MonoidalCategory.Arrow.PullbackHom.isInitialIso X i).inv.left =
    CategoryTheory.CategoryStruct.id (W ⟹ X.left)
-- Init.Data.Array.MapIdx
Array.mapIdx_setIfInBounds : ∀ {α : Type u_1} {α_1 : Type u_2} {f : ℕ → α → α_1} {xs : Array α} {i : ℕ} {a : α},
  Array.mapIdx f (xs.setIfInBounds i a) = (Array.mapIdx f xs).setIfInBounds i (f i a)
-- Mathlib.Data.Set.Lattice
iSup_iUnion : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_5} [inst : CompleteLattice β] (s : ι → Set α) (f : α → β),
  ⨆ a ∈ ⋃ i, s i, f a = ⨆ i, ⨆ a ∈ s i, f a
-- Std.Tactic.BVDecide.LRAT.Parser
Std.Tactic.BVDecide.LRAT.Parser.Binary.parseAction : Std.Internal.Parsec.ByteArray.Parser Std.Tactic.BVDecide.LRAT.IntAction
-- Init.Data.String.Lemmas.Pattern.String.Basic
String.Slice.Pattern.Model.ForwardStringSearcher.instNoPrefixPatternModel : ∀ {pat : String}, String.Slice.Pattern.Model.NoPrefixPatternModel pat
-- Mathlib.Combinatorics.Quiver.Subquiver
Quiver.Total.mk.inj : ∀ {V : Type u} {inst : Quiver V} {left right : V} {hom : left ⟶ right} {left_1 right_1 : V} {hom_1 : left_1 ⟶ right_1},
  { left := left, right := right, hom := hom } = { left := left_1, right := right_1, hom := hom_1 } →
    left = left_1 ∧ right = right_1 ∧ hom ≍ hom_1
-- Mathlib.Probability.Independence.Kernel.Indep
ProbabilityTheory.Kernel.iIndep_congr : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {m : ι → MeasurableSpace Ω}
  {_mΩ : MeasurableSpace Ω} {κ η : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α},
  ⇑κ =ᵐ[μ] ⇑η → (ProbabilityTheory.Kernel.iIndep m κ μ ↔ ProbabilityTheory.Kernel.iIndep m η μ)
-- Mathlib.RingTheory.HahnSeries.Basic
HahnSeries.eq_of_mem_support_single : ∀ {Γ : Type u_1} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : Zero R] {a : Γ} {r : R} {b : Γ},
  b ∈ ((HahnSeries.single a) r).support → b = a
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
HasDerivAt.sinh : ∀ {f : ℝ → ℝ} {f' x : ℝ}, HasDerivAt f f' x → HasDerivAt (fun x => Real.sinh (f x)) (Real.cosh (f x) * f') x
-- Mathlib.Data.SetLike.Basic
IsConcreteLE.mk : ∀ {A : Type u_1} {B : outParam (Type u_2)} [inst : SetLike A B] [inst_1 : LE A],
  (∀ {S T : A}, ↑S ⊆ ↑T ↔ S ≤ T) → IsConcreteLE A B
-- Lean.Meta.Tactic.SolveByElim
/-- Try calling `constructor` if no lemmas apply.  -/
Lean.Meta.SolveByElim.SolveByElimConfig.constructor : Lean.Meta.SolveByElim.SolveByElimConfig → Bool
-- Mathlib.Algebra.Tropical.BigOperators
untrop_prod : ∀ {R : Type u_1} {S : Type u_2} [inst : AddCommMonoid R] (s : Finset S) (f : S → Tropical R),
  Tropical.untrop (∏ i ∈ s, f i) = ∑ i ∈ s, Tropical.untrop (f i)
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrpObj.neg_def : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C],
  CategoryTheory.AddGrpObj.neg = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
-- Mathlib.RingTheory.Polynomial.IsIntegral
/-- [Stacks Tag 00H6](https://stacks.math.columbia.edu/tag/00H6) ((1)) -/
Polynomial.isIntegral_coeff_of_dvd : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Polynomial R)
  (q : Polynomial S), p.Monic → q.Monic → q ∣ Polynomial.map (algebraMap R S) p → ∀ (i : ℕ), IsIntegral R (q.coeff i)
-- Mathlib.Topology.MetricSpace.Lipschitz
LipschitzOnWith.le_add_mul : ∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α} {f : α → ℝ} {K : NNReal},
  LipschitzOnWith K f s → ∀ {x : α}, x ∈ s → ∀ {y : α}, y ∈ s → f x ≤ f y + ↑K * dist x y
-- Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
/-- If all but one object in a diagram is strict terminal, then the limit is isomorphic to the
said object via `limit.π`.  -/
CategoryTheory.Limits.limit_π_isIso_of_is_strict_terminal : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasStrictTerminalObjects C] {J : Type v}
  [inst_2 : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J C) [inst_3 : CategoryTheory.Limits.HasLimit F]
  (i : J) (H : (j : J) → j ≠ i → CategoryTheory.Limits.IsTerminal (F.obj j)) [Subsingleton (i ⟶ i)],
  CategoryTheory.IsIso (CategoryTheory.Limits.limit.π F i)
-- Mathlib.MeasureTheory.Measure.WithDensityFinite
MeasureTheory.instIsFiniteMeasureToFinite : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : MeasureTheory.SFinite μ],
  MeasureTheory.IsFiniteMeasure μ.toFinite
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.image_one : ∀ {α : Type u_2} {β : Type u_3} [inst : One α] {f : α → β}, f '' 1 = {f 1}