mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.Monoid.Unbundled.Pow
pow_lt_pow_left' : ∀ {M : Type u_3} [inst : Monoid M] [inst_1 : Preorder M] [MulLeftStrictMono M] [MulRightStrictMono M] {n : ℕ},
  n ≠ 0 → ∀ {a b : M}, a < b → a ^ n < b ^ n
-- Std.Time.Internal.Bounded
/-- Adjust the bounds of a `Bounded` by applying the multiplication operation with a positive number.
 -/
Std.Time.Internal.Bounded.LE.mul_pos : {n m : ℤ} → Std.Time.Internal.Bounded.LE n m → (num : ℤ) → num ≥ 0 → Std.Time.Internal.Bounded.LE (n * num) (m * num)
-- Mathlib.LinearAlgebra.Projectivization.Subspace
Projectivization.Subspace.mem_add : ∀ {K : Type u_1} {V : Type u_2} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  (T : Projectivization.Subspace K V) (v w : V) (hv : v ≠ 0) (hw : w ≠ 0) (hvw : v + w ≠ 0),
  Projectivization.mk K v hv ∈ T → Projectivization.mk K w hw ∈ T → Projectivization.mk K (v + w) hvw ∈ T
-- Std.Data.DHashMap.Internal.RawLemmas
_private.Std.Data.DHashMap.Internal.RawLemmas.0.Std.DHashMap.Raw.insert.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (m : Std.DHashMap.Raw α β) (a : α) (b : β a),
  m.insert a b = if h : 0 < m.buckets.size then ↑(Std.DHashMap.Internal.Raw₀.insert ⟨m, h⟩ a b) else m
-- Mathlib.RingTheory.Support
Module.mem_support_iff : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {p : PrimeSpectrum R}, p ∈ Module.support R M ↔ Nontrivial (LocalizedModule p.asIdeal.primeCompl M)
-- Mathlib.Data.Finset.Lattice.Fold
/-- **Alias** of `Finset.apply_sup_eq_sup_comp`. -/
Finset.comp_sup_eq_sup_comp : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : SemilatticeSup α] [inst_1 : OrderBot α]
  [inst_2 : SemilatticeSup γ] [inst_3 : OrderBot γ] {s : Finset β} {f : β → α} (g : α → γ),
  (∀ (x y : α), g (x ⊔ y) = g x ⊔ g y) → g ⊥ = ⊥ → g (s.sup f) = s.sup (g ∘ f)
-- Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Polynomial.le_trailingDegree_X : ∀ {R : Type u} [inst : Semiring R], 1 ≤ Polynomial.X.trailingDegree
-- Mathlib.Algebra.Category.Grp.Biproducts
AddCommGrpCat.biprodIsoProd_inv_comp_fst_apply : ∀ (G H : AddCommGrpCat) (x : ↑G × ↑H),
  (CategoryTheory.ConcreteCategory.hom CategoryTheory.Limits.biprod.fst)
      ((CategoryTheory.ConcreteCategory.hom (G.biprodIsoProd H).inv) x) =
    x.1
-- Mathlib.Combinatorics.HalesJewett
Combinatorics.Subspace.mk.congr_simp : ∀ {η : Type u_5} {α : Type u_6} {ι : Type u_7} (idxFun idxFun_1 : ι → α ⊕ η) (e_idxFun : idxFun = idxFun_1)
  (proper : ∀ (e : η), ∃ i, idxFun i = Sum.inr e),
  { idxFun := idxFun, proper := proper } = { idxFun := idxFun_1, proper := ⋯ }
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.one_lt_rpow_iff : ∀ {x y : ℝ}, 0 ≤ x → (1 < x ^ y ↔ 1 < x ∧ 0 < y ∨ 0 < x ∧ x < 1 ∧ y < 0)
-- Mathlib.Data.Nat.Cast.Defs
/-- Addition is commutative in a commutative additive magma.  -/
AddCommMonoidWithOne.add_comm : ∀ {R : Type u_2} [self : AddCommMonoidWithOne R] (a b : R), a + b = b + a
-- Mathlib.Algebra.Polynomial.Derivative
Polynomial.coeff_derivative : ∀ {R : Type u} [inst : Semiring R] (p : Polynomial R) (n : ℕ),
  (Polynomial.derivative p).coeff n = p.coeff (n + 1) * (↑n + 1)
-- Init.Grind.FieldNormNum
Lean.Grind.Field.NormNum.eq_int : ∀ {α : Type u_1} [inst : Lean.Grind.Field α] (a : α) (v : ℚ) (n : ℤ),
  (n == v.num && v.den == 1) = true → a = Lean.Grind.Field.NormNum.ofRat v → a = IntCast.intCast n
-- Mathlib.CategoryTheory.IsConnected
/-- If any two objects in a nonempty category are linked by a sequence of (potentially reversed)
morphisms, then J is connected.

The converse of `exists_zigzag'`.
 -/
CategoryTheory.isPreconnected_of_zigzag : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J],
  (∀ (j₁ j₂ : J), ∃ l, List.IsChain CategoryTheory.Zag (j₁ :: l) ∧ (j₁ :: l).getLast ⋯ = j₂) →
    CategoryTheory.IsPreconnected J
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.mul_vle_mul_iff_left : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R] {x y z : R}, 0 <ᵥ z → (x * z ≤ᵥ y * z ↔ x ≤ᵥ y)
-- Init.Data.Subtype.Order
Subtype.instAntisymmLE : ∀ {α : Type u} [inst : LE α] [i : Std.Antisymm fun x1 x2 => x1 ≤ x2] {P : α → Prop}, Std.Antisymm fun x1 x2 => x1 ≤ x2
-- Init.GrindInstances.ToInt
Lean.Grind.instLTUInt32UintOfNatNat : Lean.Grind.ToInt.LT UInt32 (Lean.Grind.IntInterval.uint 32)
-- Mathlib.Analysis.RCLike.Basic
RCLike.I_re_ax : ∀ {K : semiOutParam (Type u_1)} [self : RCLike K], RCLike.re RCLike.I = 0
-- Mathlib.LinearAlgebra.TensorProduct.Map
LinearMap.lTensor_mul : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Type u_7) {N : Type u_8} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] (f g : Module.End R N),
  LinearMap.lTensor M (f * g) = LinearMap.lTensor M f * LinearMap.lTensor M g
-- Mathlib.Data.Multiset.MapFold
Multiset.map_id : ∀ {α : Type u_1} (s : Multiset α), Multiset.map id s = s
-- Mathlib.NumberTheory.LSeries.HurwitzZetaEven
/-- Formula for `completedCosZeta` as a Dirichlet series in the convergence range
(first version, with sum over `ℤ`).  -/
HurwitzZeta.hasSum_int_completedCosZeta : ∀ (a : ℝ) {s : ℂ},
  1 < s.re →
    HasSum (fun n => s.Gammaℝ * Complex.exp (2 * ↑Real.pi * Complex.I * ↑a * ↑n) / ↑|n| ^ s / 2)
      (HurwitzZeta.completedCosZeta (↑a) s)
-- Mathlib.Topology.Algebra.OpenSubgroup
Subgroup.instFiniteQuotientSubtypeMemOpenSubgroupOfIsTopologicalGroupOfCompactSpace : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G]
  (U : OpenSubgroup G) (K : OpenSubgroup ↥U), Finite (↥U ⧸ ↑K)
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.distortion_bot : ∀ {ι : Type u_1} [inst : Fintype ι] (I : BoxIntegral.Box ι), ⊥.distortion = 0
-- Aesop.Frontend.Basic
Lean.Parser.Category.Aesop.bool_lit : Lean.Parser.Category
-- Mathlib.Geometry.Manifold.LocalInvariantProperties
StructureGroupoid.LocalInvariantProp.liftPropWithinAt_indep_chart_source_aux : ∀ {H : Type u_1} {M : Type u_2} {H' : Type u_3} [inst : TopologicalSpace H] [inst_1 : TopologicalSpace M]
  [inst_2 : ChartedSpace H M] [inst_3 : TopologicalSpace H'] {G : StructureGroupoid H} {G' : StructureGroupoid H'}
  {e : OpenPartialHomeomorph M H} {P : (H → H') → Set H → H → Prop} {s : Set M} {x : M},
  G.LocalInvariantProp G' P →
    ∀ (g : M → H'),
      e ∈ StructureGroupoid.maximalAtlas M G →
        x ∈ e.source →
          (P (g ∘ ↑(chartAt H x).symm) (↑(chartAt H x).symm ⁻¹' s) (↑(chartAt H x) x) ↔
            P (g ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x))
-- Mathlib.NumberTheory.Cyclotomic.Basic
/-- Two elements in the Galois group of a cyclotomic extension are equal if
their actions on primitive roots are equal.  -/
IsCyclotomicExtension.algEquiv_eq_of_apply_eq : ∀ (S : Set ℕ) (A : Type u) (B : Type v) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B]
  [IsCyclotomicExtension S A B] [IsDomain B] {f g : B ≃ₐ[A] B},
  (∀ n ∈ S, n ≠ 0 → ∃ r, IsPrimitiveRoot r n ∧ f r = g r) → f = g
-- Mathlib.Tactic.IntervalCases
Mathlib.Tactic.IntervalCases.of_le_right : ∀ {α : Type u_1} {a b b' : α} [inst : LE α], a ≤ b → b = b' → a ≤ b'
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.comp_snd : ∀ {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 Y Z : CategoryTheory.Limits.CategoricalPullback F G} (f : X.Hom Y) (g : Y.Hom Z),
  (CategoryTheory.CategoryStruct.comp f g).snd = CategoryTheory.CategoryStruct.comp f.snd g.snd
-- Mathlib.Topology.ContinuousMap.ZeroAtInfty
/-- The type of continuous functions vanishing at infinity, with the uniform distance induced by the
inclusion `ZeroAtInftyContinuousMap.toBCF`, is a metric space.  -/
ZeroAtInftyContinuousMap.instMetricSpace : {α : Type u} →
  [inst : TopologicalSpace α] →
    {β : Type u_2} → [inst_1 : MetricSpace β] → [inst_2 : Zero β] → MetricSpace (ZeroAtInftyContinuousMap α β)
-- Mathlib.Data.Ordmap.Ordset
Ordnode.Valid'.rotateL_lemma₃ : ∀ {a b c : ℕ}, 3 * a ≤ b + c → b < 2 * c → a + b < 3 * c
-- Mathlib.GroupTheory.ArchimedeanDensely
Int.card_fintype_addEquiv : Fintype.card (ℤ ≃+ ℤ) = 2
-- Mathlib.RingTheory.NonUnitalSubring.Basic
/-- `closure` forms a Galois insertion with the coercion to set.  -/
NonUnitalSubring.gi : (R : Type u) → [inst : NonUnitalNonAssocRing R] → GaloisInsertion NonUnitalSubring.closure SetLike.coe
-- Init.Prelude
/-- Resolves the given name to an overload list of global definitions.
The `List String` in each alternative is the deduced list of projections
(which are ambiguous with name components).  -/
Lean.Macro.Methods.resolveGlobalName : Lean.Macro.Methods → Lean.Name → Lean.MacroM (List (Lean.Name × List String))
-- Mathlib.Data.Nat.Bits
Nat.shiftLeft'_false : ∀ {m : ℕ} (n : ℕ), Nat.shiftLeft' false m n = m <<< n
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
/-- Composition of continuous linear maps, as a bilinear map. Compare `LinearMap.llcomp`.  -/
ContinuousLinearMap.llcomp : (R : Type u_1) →
  (U : Type u_2) →
    (V : Type u_3) →
      (W : Type u_4) →
        [inst : CommSemiring R] →
          [inst_1 : AddCommMonoid U] →
            [inst_2 : Module R U] →
              [inst_3 : TopologicalSpace U] →
                [inst_4 : AddCommMonoid V] →
                  [inst_5 : Module R V] →
                    [inst_6 : TopologicalSpace V] →
                      [inst_7 : ContinuousAdd V] →
                        [inst_8 : ContinuousConstSMul R V] →
                          [inst_9 : AddCommMonoid W] →
                            [inst_10 : Module R W] →
                              [inst_11 : TopologicalSpace W] →
                                [inst_12 : ContinuousAdd W] →
                                  [inst_13 : ContinuousConstSMul R W] → (U →L[R] V) →ₗ[R] (V →L[R] W) →ₗ[R] U →L[R] W
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.maxKey?_modify_eq_maxKey? : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp], t.WF → ∀ {k : α} {f : β → β}, (Std.DTreeMap.Raw.Const.modify t k f).maxKey? = t.maxKey?
-- Mathlib.Topology.Algebra.Monoid
Filter.Tendsto.pow : ∀ {α : Type u_2} {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : Monoid M] [ContinuousMul M] {l : Filter α}
  {f : α → M} {x : M}, Filter.Tendsto f l (nhds x) → ∀ (n : ℕ), Filter.Tendsto (fun x => f x ^ n) l (nhds (x ^ n))
-- Mathlib.Order.Comparable
incompRel_comm : ∀ {α : Type u_1} {r : α → α → Prop} {a b : α}, IncompRel r a b ↔ IncompRel r b a
-- Mathlib.CategoryTheory.ComposableArrows.Four
CategoryTheory.ComposableArrows.fourδ₁Toδ₀_app_three : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {i₀ i₁ i₂ i₃ i₄ : C} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂)
  (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₁₂ : i₀ ⟶ i₂) (h₁₂ : CategoryTheory.CategoryStruct.comp f₁ f₂ = f₁₂),
  (CategoryTheory.ComposableArrows.fourδ₁Toδ₀ f₁ f₂ f₃ f₄ f₁₂ h₁₂).app 3 =
    CategoryTheory.CategoryStruct.id ((CategoryTheory.ComposableArrows.mk₃ f₁₂ f₃ f₄).obj 3)
-- Mathlib.Probability.Process.Stopping
MeasureTheory.stoppedProcess_const_bot : ∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : Nonempty ι] {u : ι → Ω → β} [inst_1 : LinearOrder ι]
  [inst_2 : OrderBot ι], (MeasureTheory.stoppedProcess u fun x => ⊥) = fun x => u ⊥
-- Mathlib.MeasureTheory.MeasurableSpace.Prod
/-- If `C` and `D` generate the σ-algebras on `α` resp. `β`, then rectangles formed by `C` and `D`
generate the σ-algebra on `α × β`.  -/
generateFrom_eq_prod : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {C : Set (Set α)}
  {D : Set (Set β)},
  MeasurableSpace.generateFrom C = inst →
    MeasurableSpace.generateFrom D = inst_1 →
      IsCountablySpanning C →
        IsCountablySpanning D →
          MeasurableSpace.generateFrom (Set.image2 (fun x1 x2 => x1 ×ˢ x2) C D) = Prod.instMeasurableSpace
-- Init.Data.Int.Basic
Int.ofNat.sizeOf_spec : ∀ (a : ℕ), sizeOf (Int.ofNat a) = 1 + sizeOf a
-- Mathlib.Geometry.Manifold.ContMDiff.Defs
ContMDiff.contMDiffOn : ∀ {𝕜 : 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] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {s : Set M}
  {n : WithTop ℕ∞}, ContMDiff I I' n f → ContMDiffOn I I' n f s
-- Lean.Server.ServerTask
Lean.Server.ServerTask.IO.bindTaskCostly : {α : Type u_1} →
  {β : Type} →
    Lean.Server.ServerTask α →
      (α → IO (Lean.Server.ServerTask (Except IO.Error β))) → BaseIO (Lean.Server.ServerTask (Except IO.Error β))
-- Mathlib.RingTheory.Coalgebra.Convolution
LinearMap.toSpanSingleton_convMul_toSpanSingleton : ∀ {R : Type u_1} {A : Type u_3} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  [inst_3 : SMulCommClass R A A] [inst_4 : IsScalarTower R A A] (x y : A),
  WithConv.toConv (LinearMap.toSpanSingleton R A x) * WithConv.toConv (LinearMap.toSpanSingleton R A y) =
    WithConv.toConv (LinearMap.toSpanSingleton R A (x * y))
-- Mathlib.Analysis.Asymptotics.TVS
ContinuousLinearMap.isBigOTVS_id : ∀ {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : TopologicalSpace E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommGroup F] [inst_5 : TopologicalSpace F]
  [inst_6 : Module 𝕜 F] {l : Filter E} (f : E →L[𝕜] F), ⇑f =O[𝕜; l] id
-- Mathlib.Order.Hom.Bounded
TopHom.coe_sup : ∀ {α : Type u_2} {β : Type u_3} [inst : Top α] [inst_1 : SemilatticeSup β] [inst_2 : OrderTop β] (f g : TopHom α β),
  ⇑(f ⊔ g) = ⇑f ⊔ ⇑g
-- Init.Data.Range.Polymorphic.SInt
Int8.instRxiIsAlwaysFinite : Std.Rxi.IsAlwaysFinite Int8
-- Mathlib.Algebra.Homology.Homotopy
Homotopy.mk.injEq : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {c : ComplexShape ι} {C D : HomologicalComplex V c} {f g : C ⟶ D} (hom : (i j : ι) → C.X i ⟶ D.X j)
  (zero : autoParam (∀ (i j : ι), ¬c.Rel j i → hom i j = 0) Homotopy.zero._autoParam)
  (comm : autoParam (∀ (i : ι), f.f i = (dNext i) hom + (prevD i) hom + g.f i) Homotopy.comm._autoParam)
  (hom_1 : (i j : ι) → C.X i ⟶ D.X j)
  (zero_1 : autoParam (∀ (i j : ι), ¬c.Rel j i → hom_1 i j = 0) Homotopy.zero._autoParam)
  (comm_1 : autoParam (∀ (i : ι), f.f i = (dNext i) hom_1 + (prevD i) hom_1 + g.f i) Homotopy.comm._autoParam),
  ({ hom := hom, zero := zero, comm := comm } = { hom := hom_1, zero := zero_1, comm := comm_1 }) = (hom = hom_1)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey?_insert : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {a k : α} {v : β},
  (t.insert k v).getKey? a = if cmp k a = Ordering.eq then some k else t.getKey? a
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
SubMulAction.ofFixingSubgroup_of_inclusion.eq_1 : ∀ (M : Type u_1) {α : Type u_2} [inst : Group M] [inst_1 : MulAction M α] {s t : Set α} (hst : t ⊆ s),
  SubMulAction.ofFixingSubgroup_of_inclusion M hst = { toFun := fun y => ⟨↑y, ⋯⟩, map_smul' := ⋯ }
-- Mathlib.CategoryTheory.Subobject.Limits
CategoryTheory.Limits.imageSubobject_arrow : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasImage f],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobjectIso f).hom (CategoryTheory.Limits.image.ι f) =
    (CategoryTheory.Limits.imageSubobject f).arrow
-- Init.Internal.Order.Basic
/-- Park induction for least fixpoint of a monotone function `f`.
Takes an explicit witness of `f` being monotone.
 -/
Lean.Order.lfp_le_of_le_monotone : ∀ {α : Sort u} [inst : Lean.Order.CompleteLattice α] (f : α → α) {hm : Lean.Order.monotone f} (x : α),
  Lean.Order.PartialOrder.rel (f x) x → Lean.Order.PartialOrder.rel (Lean.Order.lfp_monotone f hm) x
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
hasSum_pnat_iff_hasSum_succ : ∀ {M : Type u_1} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M] {m : M} {f : ℕ → M},
  HasSum (fun x => f ↑x) m ↔ HasSum (fun x => f (x + 1)) m
-- Mathlib.FieldTheory.Fixed
FixedPoints.isIntegral : ∀ (G : Type u) [inst : Group G] (F : Type v) [inst_1 : Field F] [inst_2 : MulSemiringAction G F] [Finite G] (x : F),
  IsIntegral (↥(FixedPoints.subfield G F)) x
-- Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
/-- A matrix whose nondiagonal entries are negative with the sum of the entries of each
row positive has nonzero determinant.  -/
Matrix.det_ne_zero_of_sum_row_pos : ∀ {n : Type u_1} [inst : Fintype n] [inst_1 : DecidableEq n] {S : Type u_2} [inst_2 : CommRing S]
  [inst_3 : LinearOrder S] [IsStrictOrderedRing S] {A : Matrix n n S},
  (Pairwise fun i j => A i j < 0) → (∀ (i : n), 0 < ∑ j, A i j) → A.det ≠ 0
-- Mathlib.Algebra.Group.Equiv.Basic
/-- The isomorphism `(M →* N₁) ≃* (M →* N₂)` obtained by postcomposition with
a multiplicative equivalence `e : N₁ ≃* N₂`.  -/
MulEquiv.monoidHomCongrRight : {M : Type u_4} →
  {N₁ : Type u_9} →
    {N₂ : Type u_10} →
      [inst : MulOneClass M] → [inst_1 : CommMonoid N₁] → [inst_2 : CommMonoid N₂] → N₁ ≃* N₂ → (M →* N₁) ≃* (M →* N₂)
-- Mathlib.Algebra.Order.Floor.Ring
Int.ceil_one : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] [IsOrderedRing R], ⌈1⌉ = 1
-- Init.Grind.Module.Basic
Lean.Grind.AddCommGroup.neg_eq_zero : ∀ {M : Type u} [inst : Lean.Grind.AddCommGroup M] (a : M), -a = 0 ↔ a = 0
-- Mathlib.Analysis.LocallyConvex.Basic
absorbs_iff_eventually_nhdsNE_zero : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : NormedDivisionRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  {s t : Set E}, Absorbs 𝕜 s t ↔ ∀ᶠ (c : 𝕜) in nhdsWithin 0 {0}ᶜ, Set.MapsTo (fun x => c • x) t s
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.get?_union : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α}, (m₁ ∪ m₂).get? k = (m₂.get? k).or (m₁.get? k)
-- Mathlib.AlgebraicGeometry.Birational.Birational
/-- Compose two partial isomorphisms along a proof that the target of `f` equals the source
of `g`. See `trans` for the version that does not require this.  -/
AlgebraicGeometry.Scheme.PartialIso.trans' : {X Y Z : AlgebraicGeometry.Scheme} → (f : X.PartialIso Y) → (g : Y.PartialIso Z) → f.target = g.source → X.PartialIso Z
-- Lean.Widget.Types
/-- Arguments to be passed to the component's default exported function.
Must be a JSON object.

In certain contexts
(such as when rendering as a panel widget; see `Widget.savePanelWidgetInfo`),
the Lean infoview appends additional fields to this object.

Props may contain RPC references,
so must be stored as a `StateM` computation
with access to the RPC object store.  -/
Lean.Widget.WidgetInstance.props : Lean.Widget.WidgetInstance → StateM Lean.Server.RpcObjectStore Lean.Json
-- Mathlib.Topology.Bornology.Basic
/-- The filter of cobounded sets in a bornology.  -/
Bornology.cobounded : (α : Type u_4) → [self : Bornology α] → Filter α
-- Init.Control.ExceptCps
/-- For continuation monads, it is not possible to provide a computable `MonadAttach` instance that
actually adds information about the return value. Therefore, this instance always attaches a proof
of `True`.
 -/
ExceptCpsT.instMonadAttach : {ε : Type u_1} → {m : Type u_1 → Type u_2} → MonadAttach (ExceptCpsT ε m)
-- Mathlib.CategoryTheory.Comma.StructuredArrow.CommaMap
/-- The structured arrow category on the functor `Comma.map α β`, with `β` a natural isomorphism,
is equivalent to a comma category on two instances of `StructuredArrow.map₂`.  -/
CategoryTheory.StructuredArrow.commaMapEquivalence : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {T : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} T] →
            {L : CategoryTheory.Functor C T} →
              {R : CategoryTheory.Functor D T} →
                {C' : Type u₄} →
                  [inst_3 : CategoryTheory.Category.{v₄, u₄} C'] →
                    {D' : Type u₅} →
                      [inst_4 : CategoryTheory.Category.{v₅, u₅} D'] →
                        {T' : Type u₆} →
                          [inst_5 : CategoryTheory.Category.{v₆, u₆} T'] →
                            {L' : CategoryTheory.Functor C' T'} →
                              {R' : CategoryTheory.Functor D' T'} →
                                {F₁ : CategoryTheory.Functor C C'} →
                                  {F₂ : CategoryTheory.Functor D D'} →
                                    {F : CategoryTheory.Functor T T'} →
                                      (α : F₁.comp L' ⟶ L.comp F) →
                                        (β : R.comp F ⟶ F₂.comp R') →
                                          [inst_6 : CategoryTheory.IsIso β] →
                                            (X : CategoryTheory.Comma L' R') →
                                              CategoryTheory.StructuredArrow X (CategoryTheory.Comma.map α β) ≌
                                                CategoryTheory.Comma
                                                  (CategoryTheory.StructuredArrow.map₂
                                                    (CategoryTheory.CategoryStruct.id (L'.obj X.left)) α)
                                                  (CategoryTheory.StructuredArrow.map₂ X.hom (CategoryTheory.inv β))
-- Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq
Real.dist_mulExpNegMulSq_le_two_mul_sqrt : ∀ {ε : ℝ}, 0 < ε → ∀ (x y : ℝ), dist (ε.mulExpNegMulSq x) (ε.mulExpNegMulSq y) ≤ 2 * (√ε)⁻¹
-- Mathlib.Analysis.Calculus.FDeriv.Basic
HasFDerivAtFilter.isTheta_sub : ∀ {𝕜 : 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] {f : E → F}
  {f' : E →L[𝕜] F} {L : Filter (E × E)},
  HasFDerivAtFilter f f' L → Topology.IsInducing ⇑f' → (fun p => f p.1 - f p.2) =Θ[L] fun p => p.1 - p.2
-- Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
CategoryTheory.MorphismProperty.Under.map_map_right : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] {P : CategoryTheory.MorphismProperty T}
  (Q : CategoryTheory.MorphismProperty T) [inst_1 : Q.IsMultiplicative] {X Y : T} [inst_2 : P.IsStableUnderComposition]
  {f : X ⟶ Y} (hPf : P f)
  {X_1 Y_1 :
    CategoryTheory.MorphismProperty.Comma (CategoryTheory.Functor.fromPUnit Y) (CategoryTheory.Functor.id T) P ⊤ Q}
  (f_1 : X_1 ⟶ Y_1),
  ((CategoryTheory.MorphismProperty.Under.map Q hPf).map f_1).right =
    (CategoryTheory.MorphismProperty.Comma.Hom.hom f_1).right
-- Mathlib.Algebra.Order.Archimedean.Class
FiniteMulArchimedeanClass.mem_closedBallSubgroup_iff : ∀ {M : Type u_1} [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M] {a : M}
  {c : FiniteMulArchimedeanClass M}, a ∈ c.closedBallSubgroup ↔ ∀ (h : a ≠ 1), c ≤ FiniteMulArchimedeanClass.mk a h
-- Mathlib.Data.Nat.Bits
Nat.bit_ne_zero : ∀ (b : Bool) {n : ℕ}, n ≠ 0 → Nat.bit b n ≠ 0
-- Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Complex.log_sub_logTaylor_isBigO : ∀ (n : ℕ), (fun z => Complex.log (1 + z) - Complex.logTaylor (n + 1) z) =O[nhds 0] fun z => z ^ (n + 1)