mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Probability.Moments.SubGaussian
ProbabilityTheory.Kernel.HasSubgaussianMGF.measure_pos_eq_zero_of_hasSubGaussianMGF_zero : ∀ {Ω : Type u_1} {Ω' : Type u_2} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} {ν : MeasureTheory.Measure Ω'}
  {κ : ProbabilityTheory.Kernel Ω' Ω} {X : Ω → ℝ},
  ProbabilityTheory.Kernel.HasSubgaussianMGF X 0 κ ν → ∀ᵐ (ω' : Ω') ∂ν, (κ ω') {ω | 0 < X ω} = 0
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2.SupportsStmt.eq_5 : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} (S : Finset Λ) (a : σ → Bool)
  (q₁ q₂ : Turing.TM2.Stmt Γ Λ σ),
  Turing.TM2.SupportsStmt S (Turing.TM2.Stmt.branch a q₁ q₂) =
    (Turing.TM2.SupportsStmt S q₁ ∧ Turing.TM2.SupportsStmt S q₂)
-- Mathlib.SetTheory.Ordinal.Notation
_private.Mathlib.SetTheory.Ordinal.Notation.0.ONote.fastGrowing.match_1.eq_3 : ∀ (o : ONote) (motive : (x : Option ONote ⊕ (ℕ → ONote)) → o.FundamentalSequenceProp x → Sort u_1) (f : ℕ → ONote)
  (h : o.FundamentalSequenceProp (Sum.inr f))
  (h_1 : (x : o.FundamentalSequenceProp (Sum.inl none)) → motive (Sum.inl none) x)
  (h_2 : (a : ONote) → (h : o.FundamentalSequenceProp (Sum.inl (some a))) → motive (Sum.inl (some a)) h)
  (h_3 : (f : ℕ → ONote) → (h : o.FundamentalSequenceProp (Sum.inr f)) → motive (Sum.inr f) h),
  (match Sum.inr f, h with
    | Sum.inl none, x => h_1 x
    | Sum.inl (some a), h => h_2 a h
    | Sum.inr f, h => h_3 f h) =
    h_3 f h
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.sin_add_pi_div_two : ∀ (θ : Real.Angle), (θ + ↑(Real.pi / 2)).sin = θ.cos
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.Std.DHashMap.Internal.AssocList.map.go.eq_1 : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} (f : (a : α) → β a → γ a) (acc : Std.DHashMap.Internal.AssocList α γ),
  Std.DHashMap.Internal.AssocList.map.go✝ f acc Std.DHashMap.Internal.AssocList.nil = acc
-- Mathlib.Algebra.Group.Equiv.Opposite
AddEquiv.op_apply_apply : ∀ {α : Type u_3} {β : Type u_4} [inst : Add α] [inst_1 : Add β] (f : α ≃+ β) (a : αᵃᵒᵖ),
  (AddEquiv.op f) a = (AddOpposite.op ∘ ⇑f ∘ AddOpposite.unop) a
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toArray_roo_eq_singleton : ∀ {m n : ℕ}, n = m + 2 → (m<...n).toArray = #[m + 1]
-- Mathlib.SetTheory.Ordinal.Univ
Cardinal.small_iff_lift_mk_lt_univ : ∀ {α : Type u}, Small.{v, u} α ↔ Cardinal.lift.{v + 1, u} (Cardinal.mk α) < Cardinal.univ.{v, max u (v + 1)}
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.instEpiOpcyclesToE : ∀ {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₀ i₁ i₂ i₃ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃)
  (f₁₂ : i₀ ⟶ i₂) (h₁₂ : CategoryTheory.CategoryStruct.comp f₁ f₂ = f₁₂) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁)
  (hn₂ : n₁ + 1 = n₂), CategoryTheory.Epi (X.opcyclesToE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂)
-- Mathlib.GroupTheory.GroupAction.Defs
MulAction.selfEquivSigmaOrbits.eq_1 : ∀ (G : Type u_1) (α : Type u_2) [inst : Group G] [inst_1 : MulAction G α],
  MulAction.selfEquivSigmaOrbits G α =
    (MulAction.selfEquivSigmaOrbits' G α).trans (Equiv.sigmaCongrRight fun x => Equiv.setCongr ⋯)
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.mk_sub : ∀ {ι : Type u} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → AddGroup (β i)] {s : Finset ι}
  {x y : (i : ↑↑s) → β ↑i}, DFinsupp.mk s (x - y) = DFinsupp.mk s x - DFinsupp.mk s y
-- Init.GrindInstances.ToInt
Lean.Grind.instModBitVecUint : ∀ {v : ℕ}, Lean.Grind.ToInt.Mod (BitVec v) (Lean.Grind.IntInterval.uint v)
-- Mathlib.Logic.Equiv.Fin.Basic
finSuccEquivLast_symm_none : ∀ {n : ℕ}, finSuccEquivLast.symm none = Fin.last n
-- Mathlib.CategoryTheory.Bicategory.Functor.Oplax
/-- Oplax left unity.  -/
CategoryTheory.OplaxFunctor.map₂_leftUnitor : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (self : CategoryTheory.OplaxFunctor B C) {a b : B} (f : a ⟶ b),
  self.map₂ (CategoryTheory.Bicategory.leftUnitor f).hom =
    CategoryTheory.CategoryStruct.comp (self.mapComp (CategoryTheory.CategoryStruct.id a) f)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (self.mapId a) (self.map f))
        (CategoryTheory.Bicategory.leftUnitor (self.map f)).hom)
-- Lean.Data.Position
/-- The content of the file.  -/
Lean.FileMap.source : Lean.FileMap → String
-- Init.Data.Int.Order
Int.add_le_of_le_sub_left : ∀ {a b c : ℤ}, b ≤ c - a → a + b ≤ c
-- Mathlib.Algebra.Homology.Opposite
HomologicalComplex.unopFunctor_obj : ∀ {ι : Type u_1} (V : Type u_2) [inst : CategoryTheory.Category.{v_1, u_2} V] (c : ComplexShape ι)
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] (X : (HomologicalComplex Vᵒᵖ c)ᵒᵖ),
  (HomologicalComplex.unopFunctor V c).obj X = (Opposite.unop X).unop
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get_map : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {γ : Type w} {m : Std.DHashMap.Raw α fun x => β}
  [inst_2 : LawfulBEq α] {f : α → β → γ} {k : α} (h : m.WF) {h' : k ∈ Std.DHashMap.Raw.map f m},
  Std.DHashMap.Raw.Const.get (Std.DHashMap.Raw.map f m) k h' = f k (Std.DHashMap.Raw.Const.get m k ⋯)
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.Measure.instIsNegInvariantForallVolumeOfMeasurableNegOfSigmaFinite : ∀ {ι : Type u_1} [inst : Fintype ι] {G : ι → Type u_4} [inst_1 : (i : ι) → AddGroup (G i)]
  [inst_2 : (i : ι) → MeasureTheory.MeasureSpace (G i)] [∀ (i : ι), MeasurableNeg (G i)]
  [∀ (i : ι), MeasureTheory.SigmaFinite MeasureTheory.volume] [∀ (i : ι), MeasureTheory.volume.IsNegInvariant],
  MeasureTheory.volume.IsNegInvariant
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.C_eq_zero : ∀ {R : Type u} {σ : Type u_1} {a : R} [inst : CommSemiring R], MvPolynomial.C a = 0 ↔ a = 0
-- Std.Async.Basic
Std.Async.BaseAsync.instMonadLiftBaseIO : MonadLift BaseIO Std.Async.BaseAsync
-- Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
Subgroup.zpowers_ne_bot : ∀ {G : Type u_1} [inst : Group G] {g : G}, Subgroup.zpowers g ≠ ⊥ ↔ g ≠ 1
-- Mathlib.RingTheory.Extension.Presentation.Core
Algebra.SubmersivePresentation.map_invJacobianOfHasCoeffs : ∀ {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] [inst_3 : Finite σ] (P : Algebra.SubmersivePresentation R S ι σ) (R₀ : Type u_5)
  [inst_4 : CommRing R₀] [inst_5 : Algebra R₀ R] [inst_6 : Algebra R₀ S] [inst_7 : IsScalarTower R₀ R S]
  [inst_8 : P.HasCoeffs R₀], (MvPolynomial.map (algebraMap R₀ R)) (P.invJacobianOfHasCoeffs R₀) = P.σ ↑⋯.unit⁻¹
-- Std.Data.HashMap.Lemmas
Std.HashMap.isEmpty_map : ∀ {α : Type u} {β : Type v} {γ : Type w} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α]
  [LawfulHashable α] {f : α → β → γ}, (Std.HashMap.map f m).isEmpty = m.isEmpty
-- Init.WF
sizeOfWFRel : {α : Sort u} → [SizeOf α] → WellFoundedRelation α
-- Mathlib.Order.Bounded
Set.bounded_ge_inter_gt : ∀ {α : Type u_1} {s : Set α} [inst : LinearOrder α] (a : α),
  Set.Bounded (fun x1 x2 => x1 ≥ x2) (s ∩ {b | b < a}) ↔ Set.Bounded (fun x1 x2 => x1 ≥ x2) s
-- Mathlib.Data.Matrix.Mul
Matrix.commute_diagonal : ∀ {n : Type u_3} {α : Type u_10} [inst : NonUnitalNonAssocCommSemiring α] [inst_1 : Fintype n] [inst_2 : DecidableEq n]
  (d₁ d₂ : n → α), Commute (Matrix.diagonal d₁) (Matrix.diagonal d₂)
-- Init.Data.List.MinMax
List.min?.eq_1 : ∀ {α : Type u} [inst : Min α], [].min? = none
-- Std.Internal.Do.WP.Lemmas
_private.Std.Internal.Do.WP.Lemmas.0.OptionT.orElse.match_1.eq_2 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (x : Option α) (h_1 : (a : α) → motive (some a))
  (h_2 : (x : Option α) → motive x),
  (∀ (a : α), x = some a → False) →
    (match x with
      | some a => h_1 a
      | x => h_2 x) =
      h_2 x
-- Init.Data.Array.Lemmas
Array.eq_empty_of_append_eq_empty : ∀ {α : Type u_1} {xs ys : Array α}, xs ++ ys = #[] → xs = #[] ∧ ys = #[]
-- Lean.Meta.Eqns
_private.Lean.Meta.Eqns.0.Lean.Meta.getEqnsFor?Core : Lean.Name → Lean.MetaM (Option (Array Lean.Name))
-- Std.Data.DHashMap.Internal.Raw
_private.Std.Data.DHashMap.Internal.Raw.0.Std.DHashMap.Raw.Const.ofArray.eq_1 : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] (l : Array (α × β)),
  Std.DHashMap.Raw.Const.ofArray l = Std.DHashMap.Raw.Const.insertMany ∅ l
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Int.natAbs_sum_le : ∀ {ι : Type u_1} (s : Finset ι) (f : ι → ℤ), (∑ i ∈ s, f i).natAbs ≤ ∑ i ∈ s, (f i).natAbs
-- Mathlib.Algebra.Polynomial.Module.Basic
PolynomialModule.smul_def : ∀ {R : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (f : Polynomial R)
  (m : PolynomialModule R M),
  f • m =
    ((Polynomial.aeval
          (↑(PolynomialModule.coeffLinearEquiv R R).symm ∘ₗ
            Finsupp.lmapDomain M R Nat.succ ∘ₗ ↑(PolynomialModule.coeffLinearEquiv R R)))
        f)
      m
-- Init.Data.Range.Polymorphic.Fin
Fin.instIsAlwaysFinite : ∀ {n : ℕ}, Std.Rxc.IsAlwaysFinite (Fin n)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.AddSubMap
/-- The coefficient polynomials in linear combinations of the polynomials in `addSubMap`
that result in the fourth powers of the variables, multiplied by `W.Δ`.  -/
WeierstrassCurve.addSubMapCoeff : {R : Type u_1} → [inst : CommRing R] → WeierstrassCurve R → Fin 3 × Fin 3 → MvPolynomial (Fin 3) R
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.size_ofList : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp] {l : List (α × β)},
  List.Pairwise (fun a b => ¬cmp a.1 b.1 = Ordering.eq) l → (Std.ExtTreeMap.ofList l cmp).size = l.length
-- Mathlib.Topology.Compactness.CountablyCompact
/-- A singleton set is countably compact.  -/
isCountablyCompact_singleton : ∀ {E : Type u_2} [inst : TopologicalSpace E] {x : E}, IsCountablyCompact {x}
-- Mathlib.Data.List.FinRange
List.ofFn_eq_pmap : ∀ {α : Type u} {n : ℕ} {f : Fin n → α}, List.ofFn f = List.pmap (fun i hi => f ⟨i, hi⟩) (List.range n) ⋯
-- Mathlib.RepresentationTheory.Intertwining
Representation.IntertwiningMap.toLinearMap_tensor : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [inst : CommSemiring A] [inst_1 : Monoid G]
  [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid W] [inst_4 : AddCommMonoid U] [inst_5 : Module A V]
  [inst_6 : Module A W] [inst_7 : Module A U] {ρ : Representation A G V} {σ : Representation A G W}
  {τ : Representation A G U} {P : Type u_6} [inst_8 : AddCommMonoid P] [inst_9 : Module A P] {π : Representation A G P}
  (f : ρ.IntertwiningMap σ) (g : τ.IntertwiningMap π),
  (f.tensor g).toLinearMap = TensorProduct.map f.toLinearMap g.toLinearMap
-- Std.Time.Date.Unit.Year
Std.Time.Year.instToStringEra : ToString Std.Time.Year.Era
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.toStructuredArrow'_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) (d : D) {X Y : (CategoryTheory.CostructuredArrow F.op (Opposite.op d))ᵒᵖ}
  (f : X ⟶ Y),
  (CategoryTheory.CostructuredArrow.toStructuredArrow' F d).map f =
    CategoryTheory.StructuredArrow.homMk f.unop.left.unop ⋯
-- Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
ModelWithCorners.isBoundaryPoint_iff_not_isInteriorPoint : ∀ {𝕜 : 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] (x : M), I.IsBoundaryPoint x ↔ ¬I.IsInteriorPoint x
-- Std.Async.IO
/-- Interface for asynchronous streaming with selector-based iteration.
 -/
Std.Async.IO.AsyncStream : Type → outParam Type → Type
-- Mathlib.Tactic.ClickSuggestions.Util
Mathlib.Tactic.ClickSuggestions.Premise.const.inj : ∀ {declName declName_1 : Lean.Name},
  Mathlib.Tactic.ClickSuggestions.Premise.const declName = Mathlib.Tactic.ClickSuggestions.Premise.const declName_1 →
    declName = declName_1
-- Mathlib.Topology.Algebra.Module.FiniteDimensionBilinear
/-- Building continuous bilinear maps from bilinear functions between finite dimensional topological
vector spaces over a complete field.  -/
IsBilinearMap.toContinuousBilinearMap : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    [CompleteSpace 𝕜] →
      {E : Type u_2} →
        [inst_2 : AddCommGroup E] →
          [inst_3 : Module 𝕜 E] →
            [inst_4 : TopologicalSpace E] →
              [IsTopologicalAddGroup E] →
                [ContinuousSMul 𝕜 E] →
                  [FiniteDimensional 𝕜 E] →
                    [T2Space E] →
                      {F : Type u_3} →
                        [inst_9 : AddCommGroup F] →
                          [inst_10 : Module 𝕜 F] →
                            [inst_11 : TopologicalSpace F] →
                              [IsTopologicalAddGroup F] →
                                [ContinuousSMul 𝕜 F] →
                                  [FiniteDimensional 𝕜 F] →
                                    [T2Space F] →
                                      {G : Type u_4} →
                                        [inst_16 : AddCommGroup G] →
                                          [inst_17 : Module 𝕜 G] →
                                            [inst_18 : TopologicalSpace G] →
                                              [inst_19 : IsTopologicalAddGroup G] →
                                                [inst_20 : ContinuousSMul 𝕜 G] →
                                                  {f : E → F → G} → IsBilinearMap 𝕜 f → E →L[𝕜] F →L[𝕜] G
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalAlgebra.mem_inf : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] [inst_4 : SMulCommClass R A A] {S T : NonUnitalSubalgebra R A} {x : A},
  x ∈ S ⊓ T ↔ x ∈ S ∧ x ∈ T
-- Mathlib.Algebra.Torsor.Defs
Group.instTorsor.eq_1 : ∀ (G : Type u_1) [inst : Group G],
  Group.instTorsor G =
    { toMulAction := Monoid.toMulAction G, sdiv := Div.div, nonempty := ⋯, sdiv_smul' := ⋯, smul_sdiv' := ⋯ }
-- Lean.Meta.Sym.SynthInstance
/-- Some modules in grind use builtin instances defined directly in core (e.g., `lia`),
while others synthesize them using `synthInstance` (e.g., `ring`).
This inconsistency is problematic, as it may introduce mismatches and result in
two different representations for the same term.

The following table is used to bypass synthInstance for the builtin cases.
 -/
_private.Lean.Meta.Sym.SynthInstance.0.Lean.Meta.Sym.builtinInsts : Std.HashMap Lean.Expr Lean.Expr
-- Mathlib.LinearAlgebra.Matrix.Rank
Matrix.rank_le_width : ∀ {R : Type uR} [inst : CommSemiring R] [StrongRankCondition R] {m n : ℕ} (A : Matrix (Fin m) (Fin n) R), A.rank ≤ n
-- Mathlib.Algebra.Order.Group.Multiset
Multiset.mapAddMonoidHom_apply : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (s : Multiset α), (Multiset.mapAddMonoidHom f) s = Multiset.map f s
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsLimit.lift_comp_conePointUniqueUpToIso_hom_assoc : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {r s t : CategoryTheory.Limits.Cone F} (P : CategoryTheory.Limits.IsLimit s)
  (Q : CategoryTheory.Limits.IsLimit t) {Z : C} (h : t.pt ⟶ Z),
  CategoryTheory.CategoryStruct.comp (P.lift r)
      (CategoryTheory.CategoryStruct.comp (P.conePointUniqueUpToIso Q).hom h) =
    CategoryTheory.CategoryStruct.comp (Q.lift r) h
-- Mathlib.Data.Set.Operations
/-- `f` is bijective from `s` to `t` if `f` is injective on `s` and `f '' s = t`.  -/
Set.BijOn : {α : Type u} → {β : Type v} → (α → β) → Set α → Set β → Prop
-- Init.Data.Int.DivMod.Basic
/-- The `Div Int` and `Mod Int` instances use `Int.ediv` and `Int.emod` for compatibility with SMT-LIB and
because mathematical reasoning tends to be easier.
 -/
Int.instDiv : Div ℤ
-- Mathlib.CategoryTheory.Sites.Descent.DescentData
CategoryTheory.Pseudofunctor.DescentData.pullFunctor_map_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat) {ι : Type t} {S : C}
  {X : ι → C} {f : (i : ι) → X i ⟶ S} {S' : C} {p : S' ⟶ S} {ι' : Type t'} {X' : ι' → C} {f' : (j : ι') → X' j ⟶ S'}
  {α : ι' → ι} {p' : (j : ι') → X' j ⟶ X (α j)}
  (w : ∀ (j : ι'), CategoryTheory.CategoryStruct.comp (p' j) (f (α j)) = CategoryTheory.CategoryStruct.comp (f' j) p)
  {D₁ D₂ : F.DescentData f} (φ : D₁ ⟶ D₂) (j : ι'),
  ((CategoryTheory.Pseudofunctor.DescentData.pullFunctor F w).map φ).hom j =
    (F.map (p' j).op.toLoc).toFunctor.map (φ.hom (α j))
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.empty : ∀ {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M]
  (v : MeasureTheory.VectorMeasure α M), v ∅ = 0
-- Mathlib.Geometry.Manifold.Instances.Sphere
instIsManifoldRealEuclideanSpaceFinModelWithCornersSelfTopWithTopENatElemHAddNatOfNatSphere : ∀ (n : ℕ), IsManifold (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) ⊤ ↑(Metric.sphere 0 1)
-- Lean.Widget.InteractiveDiagnostic
Lean.Widget.MsgEmbed.goal.sizeOf_spec : ∀ (a : Lean.Widget.InteractiveGoal), sizeOf (Lean.Widget.MsgEmbed.goal a) = 1 + sizeOf a
-- Mathlib.Topology.Algebra.UniformConvergence
instMulUniformFun.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : Mul β], instMulUniformFun = { mul := instMulUniformFun._aux_1 }
-- Mathlib.Algebra.BigOperators.Option
Finset.sum_insertNone : ∀ {α : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] (f : Option α → M) (s : Finset α),
  ∑ x ∈ Finset.insertNone s, f x = f none + ∑ x ∈ s, f (some x)
-- Init.Data.UInt.Basic
instHModUInt8Nat : HMod UInt8 ℕ UInt8
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
CategoryTheory.Limits.preservesLimit_iff_isLimit_mapCone : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J] {K : CategoryTheory.Functor J C}
  {F : CategoryTheory.Functor C D} {t : CategoryTheory.Limits.Cone K} (h : CategoryTheory.Limits.IsLimit t),
  CategoryTheory.Limits.PreservesLimit K F ↔ Nonempty (CategoryTheory.Limits.IsLimit (F.mapCone t))
-- Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
/-- The limit of `n * log (1 + g n)` as `(n : ℝ) → ∞` is `t`,
where `t : ℝ` is the limit of `n * g n`.  -/
Real.tendsto_nat_mul_log_one_add_of_tendsto : ∀ {g : ℕ → ℝ} {t : ℝ},
  Filter.Tendsto (fun n => ↑n * g n) Filter.atTop (nhds t) →
    Filter.Tendsto (fun n => ↑n * Real.log (1 + g n)) Filter.atTop (nhds t)
-- Mathlib.CategoryTheory.Preadditive.Biproducts
CategoryTheory.Biprod.ofComponents_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {X₁ X₂ Y₁ Y₂ : C} (f₁₁ : X₁ ⟶ Y₁) (f₁₂ : X₁ ⟶ Y₂)
  (f₂₁ : X₂ ⟶ Y₁) (f₂₂ : X₂ ⟶ Y₂),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Biprod.ofComponents f₁₁ f₁₂ f₂₁ f₂₂)
      CategoryTheory.Limits.biprod.fst =
    CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.fst f₁₁ +
      CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.snd f₂₁
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
CategoryTheory.Limits.monoFactorisationZero_I : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] (X Y : C), (CategoryTheory.Limits.monoFactorisationZero X Y).I = 0
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKeyD_diff_of_mem_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k fallback : α}, k ∈ t₂ → (t₁ \ t₂).getKeyD k fallback = fallback
-- Mathlib.Topology.MetricSpace.Isometry
Isometry.diam_range : ∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] {f : α → β},
  Isometry f → Metric.diam (Set.range f) = Metric.diam Set.univ
-- Mathlib.Algebra.Order.Hom.Monoid
OrderMonoidIso.toOrderIso.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Mul α] [inst_3 : Mul β]
  (f : α ≃*o β), f.toOrderIso = { toEquiv := f.toEquiv, map_rel_iff' := ⋯ }
-- Mathlib.CategoryTheory.Monoidal.Internal.Module
ModuleCat.MonModuleEquivalenceAlgebra.functor_obj_carrier : ∀ {R : Type u} [inst : CommRing R] (A : CategoryTheory.Mon (ModuleCat R)),
  ↑(ModuleCat.MonModuleEquivalenceAlgebra.functor.obj A) = ↑A.X
-- Mathlib.AlgebraicGeometry.Limits
AlgebraicGeometry.isCompl_range_inl_inr : ∀ (X Y : AlgebraicGeometry.Scheme),
  IsCompl (Set.range ⇑CategoryTheory.Limits.coprod.inl) (Set.range ⇑CategoryTheory.Limits.coprod.inr)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
CategoryTheory.Functor.PushoutObjObj.ofNatIso_pt : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)} {X₁ Y₁ : C₁} {f₁ : X₁ ⟶ Y₁} {X₂ Y₂ : C₂} {f₂ : X₂ ⟶ Y₂}
  (sq : F.PushoutObjObj f₁ f₂) {F' : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)} (e : F ≅ F'),
  (sq.ofNatIso e).pt = sq.pt
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.Code.match.sizeOf_spec : ∀ (ref gen discrs optMotive : Lean.Syntax) (alts : Array (Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.Code)),
  sizeOf (Lean.Elab.Term.Do.Code.match ref gen discrs optMotive alts) =
    1 + sizeOf ref + sizeOf gen + sizeOf discrs + sizeOf optMotive + sizeOf alts
-- Aesop.Rule.Name
Aesop.DisplayRuleName.ruleName.sizeOf_spec : ∀ (n : Aesop.RuleName), sizeOf (Aesop.DisplayRuleName.ruleName n) = 1 + sizeOf n
-- Mathlib.CategoryTheory.Functor.FullyFaithful
CategoryTheory.Functor.FullyFaithful.isIso_of_isIso_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} (hF : F.FullyFaithful) {X Y : C} (f : X ⟶ Y) [CategoryTheory.IsIso (F.map f)],
  CategoryTheory.IsIso f
-- Mathlib.GroupTheory.Perm.List
List.formPerm_apply_mem_ne_self_iff : ∀ {α : Type u_1} [inst : DecidableEq α] (l : List α), l.Nodup → ∀ x ∈ l, l.formPerm x ≠ x ↔ 2 ≤ l.length
-- Mathlib.Analysis.Asymptotics.ExpGrowth
ExpGrowth.expGrowthSup_le_of_eventually_le : ∀ {u v : ℕ → ENNReal} {b : ENNReal},
  b ≠ ⊤ → (∀ᶠ (n : ℕ) in Filter.atTop, u n ≤ b * v n) → ExpGrowth.expGrowthSup u ≤ ExpGrowth.expGrowthSup v
-- Mathlib.CategoryTheory.Endofunctor.Algebra
CategoryTheory.Endofunctor.Coalgebra.Terminal.strInv.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C C}
  {A : CategoryTheory.Endofunctor.Coalgebra F} (h : CategoryTheory.Limits.IsTerminal A),
  CategoryTheory.Endofunctor.Coalgebra.Terminal.strInv h = (h.from { V := F.obj A.V, str := F.map A.str }).f
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.degree_mul_le_of_le : ∀ {R : Type u} [inst : Semiring R] {p q : Polynomial R} {a b : WithBot ℕ},
  p.degree ≤ a → q.degree ≤ b → (p * q).degree ≤ a + b
-- Mathlib.LinearAlgebra.Transvection.Basic
LinearEquiv.one_mem_transvections : ∀ {R : Type u_1} {V : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup V] [inst_2 : Module R V],
  1 ∈ LinearEquiv.transvections R V
-- Mathlib.NumberTheory.NumberField.House
_private.Mathlib.NumberTheory.NumberField.House.0.NumberField.house.asiegel.congr_simp : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] {α : Type u_2} {β : Type u_3}
  (a a_1 : Matrix α β (NumberField.RingOfIntegers K)),
  a = a_1 →
    ∀ (a_2 a_3 : α × (K →+* ℂ)),
      a_2 = a_3 →
        ∀ (a_4 a_5 : β × (K →+* ℂ)),
          a_4 = a_5 → NumberField.house.asiegel✝ K a a_2 a_4 = NumberField.house.asiegel✝ K a_1 a_3 a_5