mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RepresentationTheory.Continuous.Basic
ContRepresentation.Equiv.toContinuousLinearEquiv_inj : ∀ {R : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Monoid G] [inst_1 : Ring R]
  [inst_2 : AddCommGroup V] [inst_3 : TopologicalSpace V] [inst_4 : IsTopologicalAddGroup V] [inst_5 : Module R V]
  [inst_6 : AddCommGroup W] [inst_7 : TopologicalSpace W] [inst_8 : IsTopologicalAddGroup W] [inst_9 : Module R W]
  {ρ : ContRepresentation R G V} {σ : ContRepresentation R G W} (φ ψ : σ.Equiv ρ),
  φ.toContinuousLinearEquiv = ψ.toContinuousLinearEquiv ↔ φ = ψ
-- Mathlib.RingTheory.DedekindDomain.Different
coeIdeal_differentIdeal : ∀ (A : Type u_1) (K : Type u_2) (L : Type u) (B : Type u_3) [inst : CommRing A] [inst_1 : Field K] [inst_2 : CommRing B]
  [inst_3 : Field L] [inst_4 : Algebra A K] [inst_5 : Algebra B L] [inst_6 : Algebra A B] [inst_7 : Algebra K L]
  [inst_8 : Algebra A L] [inst_9 : IsScalarTower A K L] [inst_10 : IsScalarTower A B L] [inst_11 : IsDomain A]
  [inst_12 : IsFractionRing A K] [inst_13 : FiniteDimensional K L] [inst_14 : Algebra.IsSeparable K L]
  [inst_15 : IsIntegralClosure B A L] [inst_16 : IsIntegrallyClosed A] [inst_17 : IsDedekindDomain B]
  [inst_18 : Module.IsTorsionFree A B] [inst_19 : IsFractionRing B L],
  ↑(differentIdeal A B) = (FractionalIdeal.dual A K 1)⁻¹
-- Mathlib.MeasureTheory.Measure.Prod
AEMeasurable.prod_swap : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  [inst_2 : MeasurableSpace γ] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite μ]
  [MeasureTheory.SFinite ν] {f : β × α → γ}, AEMeasurable f (ν.prod μ) → AEMeasurable (fun z => f z.swap) (μ.prod ν)
-- Mathlib.Algebra.Polynomial.Roots
/-- A Galois connection.  -/
Multiset.prod_X_sub_C_dvd_iff_le_roots : ∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDomain R] {p : Polynomial R},
  p ≠ 0 → ∀ (s : Multiset R), (Multiset.map (fun a => Polynomial.X - Polynomial.C a) s).prod ∣ p ↔ s ≤ p.roots
-- Mathlib.Topology.MetricSpace.Bounded
IsOrderBornology.of_isCompactIcc : ∀ {α : Type u} [inst : PseudoMetricSpace α] [inst_1 : Preorder α] [CompactIccSpace α] (x : α),
  (∀ (r : ℝ), BddBelow (Metric.closedBall x r)) → (∀ (r : ℝ), BddAbove (Metric.closedBall x r)) → IsOrderBornology α
-- Mathlib.CategoryTheory.Preadditive.Opposite
CategoryTheory.Functor.unop_additive : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {D : Type u_2}
  [inst_2 : CategoryTheory.Category.{v_2, u_2} D] [inst_3 : CategoryTheory.Preadditive D]
  (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) [F.Additive], F.unop.Additive
-- Mathlib.Analysis.Convex.Combination
Finset.centerMass_insert : ∀ {R : Type u_1} {E : Type u_3} {ι : Type u_5} [inst : Field R] [inst_1 : AddCommGroup E] [inst_2 : Module R E] (i : ι)
  (t : Finset ι) {w : ι → R} (z : ι → E) [inst_3 : DecidableEq ι],
  i ∉ t →
    ∑ j ∈ t, w j ≠ 0 →
      (insert i t).centerMass w z =
        (w i / (w i + ∑ j ∈ t, w j)) • z i + ((∑ j ∈ t, w j) / (w i + ∑ j ∈ t, w j)) • t.centerMass w z
-- Mathlib.Analysis.Calculus.Gradient.Basic
hasGradientAt_iff_isLittleO : ∀ {𝕜 : Type u_1} {F : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup F] [inst_2 : InnerProductSpace 𝕜 F]
  [inst_3 : CompleteSpace F] {f : F → 𝕜} {f' x : F},
  HasGradientAt f f' x ↔ (fun x' => f x' - f x - inner 𝕜 f' (x' - x)) =o[nhds x] fun x' => x' - x
-- Init.Data.UInt.Bitwise
instIdempotentOpUInt16HAnd : Std.IdempotentOp fun x1 x2 => x1 &&& x2
-- Mathlib.RingTheory.LinearDisjoint
Subalgebra.LinearDisjoint.of_le_of_flat_left : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] {A B : Subalgebra R S},
  A.LinearDisjoint B →
    ∀ {A' B' : Subalgebra R S}, A' ≤ A → B' ≤ B → ∀ [Module.Flat R ↥A] [Module.Flat R ↥B'], A'.LinearDisjoint B'
-- Init.Grind.Module.Envelope
Lean.Grind.IntModule.OfNatModule.instIsLinearPreorderQ : ∀ {α : Type u} [inst : Lean.Grind.NatModule α] [inst_1 : LE α] [inst_2 : Std.IsLinearPreorder α]
  [inst_3 : Lean.Grind.OrderedAdd α], Std.IsLinearPreorder (Lean.Grind.IntModule.OfNatModule.Q α)
-- Mathlib.GroupTheory.Perm.List
List.formPerm_eq_of_isRotated : ∀ {α : Type u_1} [inst : DecidableEq α] {l l' : List α}, l.Nodup → l ~r l' → l.formPerm = l'.formPerm
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
SimpleGraph.unreduced_edges_subset : ∀ {α : Type u_1} {𝕜 : Type u_2} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [inst_2 : DecidableEq α] {A : Finset α}
  {P : Finpartition A} {G : SimpleGraph α} [inst_3 : DecidableRel G.Adj] {ε : 𝕜},
  {x ∈ A ×ˢ A |
      match x with
      | (x, y) => G.Adj x y ∧ ¬(SimpleGraph.regularityReduced P G (ε / 8) (ε / 4)).Adj x y} ⊆
    ((P.nonUniforms G (ε / 8)).biUnion fun x =>
          match x with
          | (U, V) => U ×ˢ V) ∪
        P.parts.biUnion Finset.offDiag ∪
      (P.sparsePairs G (ε / 4)).biUnion fun x =>
        match x with
        | (U, V) => G.interedges U V
-- Mathlib.Algebra.Homology.Factorizations.CM5a
/-- The first morphism in the factorization.  -/
_private.Mathlib.Algebra.Homology.Factorizations.CM5a.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₁.ι : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {K L : CochainComplex C ℤ} →
        (K ⟶ L) →
          [inst_2 : CategoryTheory.EnoughInjectives C] →
            (n₁ : ℤ) → K ⟶ CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₁.mid✝ K L n₁
-- Init.Data.Vector.Range
Vector.find?_range_eq_some : ∀ {n i : ℕ} {p : ℕ → Bool},
  Vector.find? p (Vector.range n) = some i ↔ p i = true ∧ i ∈ Vector.range n ∧ ∀ j < i, (!p j) = true
-- Init.Data.Array.Lemmas
Array.size_range' : ∀ {start size step : ℕ}, (Array.range' start size step).size = size
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.LeftHomologyData.liftCycles_comp_cyclesIso_hom_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (h : S.LeftHomologyData) {A : C} (k : A ⟶ S.X₂)
  (hk : CategoryTheory.CategoryStruct.comp k S.g = 0) [inst_2 : S.HasLeftHomology] {Z : C} (h_1 : h.K ⟶ Z),
  CategoryTheory.CategoryStruct.comp (S.liftCycles k hk) (CategoryTheory.CategoryStruct.comp h.cyclesIso.hom h_1) =
    CategoryTheory.CategoryStruct.comp (h.liftK k hk) h_1
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getD_diff_of_not_mem_left : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {k : α} {fallback : β k}, k ∉ t₁ → (t₁ \ t₂).getD k fallback = fallback
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.isSuccLimit_omega0 : Order.IsSuccLimit Ordinal.omega0
-- Mathlib.Topology.Algebra.InfiniteSum.Ring
HasSum.div_const : ∀ {ι : Type u_1} {α : Type u_3} {L : SummationFilter ι} [inst : DivisionSemiring α] [inst_1 : TopologicalSpace α]
  [IsTopologicalSemiring α] {f : ι → α} {a : α}, HasSum f a L → ∀ (b : α), HasSum (fun i => f i / b) (a / b) L
-- Mathlib.LinearAlgebra.Eigenspace.Basic
Module.End.hasEigenvalue_add_iff : ∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {f : Module.End R M}
  {μ ρ : R}, (f + ρ • LinearMap.id).HasEigenvalue μ ↔ f.HasEigenvalue (μ - ρ)
-- Lean.Data.Json.Parser
Lean.Json.Parser.natCore : ℕ → Std.Internal.Parsec.String.Parser ℕ
-- Mathlib.CategoryTheory.Monoidal.Closed.Ideal
CategoryTheory.bijection_symm_apply_id : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₁, u₂} D]
  (i : CategoryTheory.Functor D C) [inst_2 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_3 : CategoryTheory.Reflective i] [inst_4 : CategoryTheory.MonoidalClosed C]
  [inst_5 : CategoryTheory.CartesianMonoidalCategory D] [inst_6 : CategoryTheory.ExponentialIdeal i]
  [inst_7 : CategoryTheory.BraidedCategory C] (A B : C),
  (CategoryTheory.bijection i A B
          (CategoryTheory.MonoidalCategoryStruct.tensorObj ((CategoryTheory.reflector i).obj A)
            ((CategoryTheory.reflector i).obj B))).symm
      (CategoryTheory.CategoryStruct.id
        (CategoryTheory.MonoidalCategoryStruct.tensorObj ((CategoryTheory.reflector i).obj A)
          ((CategoryTheory.reflector i).obj B))) =
    CategoryTheory.CartesianMonoidalCategory.prodComparison (CategoryTheory.reflector i) A B
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyData.op_K : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (h : S.RightHomologyData), h.op.K = Opposite.op h.Q
-- Mathlib.Data.Erased
Erased.instLawfulMonad : LawfulMonad Erased
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKeyD_union : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k fallback : α}, (m₁ ∪ m₂).getKeyD k fallback = m₂.getKeyD k (m₁.getKeyD k fallback)
-- Mathlib.Algebra.DirectSum.Ring
/-- Multiplication from the left with any graded component's zero vanishes.  -/
DirectSum.GNonUnitalNonAssocSemiring.zero_mul : ∀ {ι : Type u_1} {A : ι → Type u_2} {inst : Add ι} {inst_1 : (i : ι) → AddCommMonoid (A i)}
  [self : DirectSum.GNonUnitalNonAssocSemiring A] {i j : ι} (b : A j), GradedMonoid.GMul.mul 0 b = 0
-- Std.Http.Data.Method
/-- Converts a `String` into a `Method`. Returns `none` for unrecognized method strings.
 -/
Std.Http.Method.ofString? : String → Option Std.Http.Method
-- Mathlib.Data.Set.Image
Set.subset_preimage_univ : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set α}, s ⊆ f ⁻¹' Set.univ
-- Mathlib.Topology.FiberBundle.Basic
/-- Preferred local trivialization of a fiber bundle constructed from core, at a given point, as
a bundle trivialization  -/
FiberBundleCore.localTrivAt : {ι : Type u_1} →
  {B : Type u_2} →
    {F : Type u_3} →
      [inst : TopologicalSpace B] →
        [inst_1 : TopologicalSpace F] → (Z : FiberBundleCore ι B F) → B → Bundle.Trivialization F Bundle.TotalSpace.proj
-- Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
/-- For `u : Opens M`, `x : u` is an interior point iff `x.val : M` is.  -/
ModelWithCorners.isInteriorPoint_iff_isInteriorPoint_val : ∀ {𝕜 : 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] {u : TopologicalSpace.Opens M} {x : ↥u},
  I.IsInteriorPoint x ↔ I.IsInteriorPoint ↑x
-- Lean.Meta.DiscrTree.Main
/-- When `noIndexAtArgs := true`, `pushArgs` assumes function application arguments have a `no_index` annotation.
That is, `f a b` is indexed as it was `f (no_index a) (no_index b)`.
This feature is used when indexing local proofs in the simplifier. This is useful in examples like the one described on issue #2670.
In this issue, we have a local hypotheses `(h : ∀ p : α × β, f p p.2 = p.2)`, and users expect it to be applicable to
`f (a, b) b = b`. This worked in Lean 3 since no indexing was used. We can retrieve Lean 3 behavior by writing
`(h : ∀ p : α × β, f p (no_index p.2) = p.2)`, but this is very inconvenient when the hypotheses was not written by the user in first place.
For example, it was introduced by another tactic. Thus, when populating the discrimination tree explicit arguments provided to `simp` (e.g., `simp [h]`),
we use `noIndexAtArgs := true`. See comment: https://github.com/leanprover/lean4/issues/2670#issuecomment-1758889365
 -/
Lean.Meta.DiscrTree.mkPathAux : Bool → Array Lean.Expr → Array Lean.Meta.DiscrTree.Key → Bool → Lean.MetaM (Array Lean.Meta.DiscrTree.Key)
-- Aesop.Tree.Data
Aesop.Goal.instNonempty : Nonempty Aesop.Goal
-- Mathlib.Algebra.Group.Action.Pointwise.Finset
Finset.smulCommClass_finset' : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : DecidableEq γ] [inst_1 : SMul α γ] [inst_2 : SMul β γ]
  [SMulCommClass α β γ], SMulCommClass α (Finset β) (Finset γ)
-- Mathlib.Control.Traversable.Basic
/-- The naturality axiom explaining how lawful traversable functors should play with
lawful applicative functors.  -/
LawfulTraversable.naturality : ∀ {t : Type u → Type u} {inst : Traversable t} [self : LawfulTraversable t] {F G : Type u → Type u}
  [inst_1 : Applicative F] [inst_2 : Applicative G] [LawfulApplicative F] [LawfulApplicative G]
  (η : ApplicativeTransformation F G) {α β : Type u} (f : α → F β) (x : t α),
  (fun {α} => η.app α) (traverse f x) = traverse ((fun {α} => η.app α) ∘ f) x
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.Dep.superset : ∀ {α : Type u_1} {M : Matroid α} {D X : Set α},
  M.Dep D → D ⊆ X → autoParam (X ⊆ M.E) Matroid.Dep.superset._auto_1 → M.Dep X
-- Mathlib.Order.Std
PartialOrder.OfStdArgs.mk.injEq : ∀ {α : Type u_1} (toPreorderArgs : Preorder.OfStdArgs α)
  (isPartialOrder :
    autoParam
      (let this := toPreorderArgs.le;
      Std.IsPartialOrder α)
      PartialOrder.OfStdArgs.isPartialOrder._autoParam)
  (toPreorderArgs_1 : Preorder.OfStdArgs α)
  (isPartialOrder_1 :
    autoParam
      (let this := toPreorderArgs_1.le;
      Std.IsPartialOrder α)
      PartialOrder.OfStdArgs.isPartialOrder._autoParam),
  ({ toPreorderArgs := toPreorderArgs, isPartialOrder := isPartialOrder } =
      { toPreorderArgs := toPreorderArgs_1, isPartialOrder := isPartialOrder_1 }) =
    (toPreorderArgs = toPreorderArgs_1)
-- Aesop.Forward.State
Aesop.VariableMap.instEmptyCollection : EmptyCollection Aesop.VariableMap
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
Equiv.sum_comp : ∀ {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [inst : Fintype ι] [inst_1 : Fintype κ] [inst_2 : AddCommMonoid M]
  (e : ι ≃ κ) (g : κ → M), ∑ i, g (e i) = ∑ i, g i
-- Mathlib.Order.CompleteLatticeIntervals
Set.Iic.coe_sInf : ∀ {α : Type u_2} [inst : CompleteLattice α] {a : α} (S : Set ↑(Set.Iic a)), ↑(sInf S) = a ⊓ sInf (Subtype.val '' S)
-- Mathlib.Topology.Algebra.Monoid
ContinuousMap.coe_mulLeft : ∀ {X : Type u_5} [inst : TopologicalSpace X] [inst_1 : Mul X] [inst_2 : SeparatelyContinuousMul X] (x : X),
  ⇑(ContinuousMap.mulLeft x) = fun y => x * y
-- Mathlib.Geometry.RingedSpace.PresheafedSpace
AlgebraicGeometry.PresheafedSpace.forget_map : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : AlgebraicGeometry.PresheafedSpace C} (f : X ⟶ Y),
  (AlgebraicGeometry.PresheafedSpace.forget C).map f = f.base
-- Mathlib.CategoryTheory.Monoidal.Opposite
/-- The equivalence between `C` and its monoidal opposite's monoidal opposite.  -/
CategoryTheory.MonoidalOpposite.mopMopEquivalence : (C : Type u₁) → [inst : CategoryTheory.Category.{v₁, u₁} C] → Cᴹᵒᵖᴹᵒᵖ ≌ C
-- Lean.Elab.Util
/-- Try to expand macro at syntax tree root and return macro declaration name and new syntax if successful.
Return none if all macros threw `Macro.Exception.unsupportedSyntax`.
 -/
Lean.Elab.expandMacroImpl? : Lean.Environment → Lean.Syntax → Lean.MacroM (Option (Lean.Name × Except Lean.Macro.Exception Lean.Syntax))
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.IsNClique.map : ∀ {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {n : ℕ} {s : Finset α},
  G.IsNClique n s → ∀ {f : α ↪ β}, (SimpleGraph.map (⇑f) G).IsNClique n (Finset.map f s)
-- Mathlib.Probability.Independence.Conditional
ProbabilityTheory.condIndep_iff : ∀ {Ω : Type u_1} (m' m₁ m₂ : MeasurableSpace Ω) {mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω] (hm' : m' ≤ mΩ),
  m₁ ≤ mΩ →
    m₂ ≤ mΩ →
      ∀ (μ : MeasureTheory.Measure Ω) [inst_1 : MeasureTheory.IsFiniteMeasure μ],
        ProbabilityTheory.CondIndep m' m₁ m₂ hm' μ ↔
          ∀ (t1 t2 : Set Ω),
            MeasurableSet t1 →
              MeasurableSet t2 →
                μ[(t1 ∩ t2).indicator fun ω => 1 | m'] =ᵐ[μ]
                  μ[t1.indicator fun ω => 1 | m'] * μ[t2.indicator fun ω => 1 | m']
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.leftExtensionEquivalenceOfIso₁_functor_obj_hom_app : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  {L L' : CategoryTheory.Functor C D} (iso₁ : L ≅ L') (F : CategoryTheory.Functor C H)
  (X : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit F) ((CategoryTheory.Functor.whiskeringLeft C D H).obj L))
  (X_1 : C),
  ((CategoryTheory.Functor.leftExtensionEquivalenceOfIso₁ iso₁ F).functor.obj X).hom.app X_1 =
    CategoryTheory.CategoryStruct.comp (X.hom.app X_1) (X.right.map (iso₁.hom.app X_1))
-- Init.Data.Nat.Power2.Lemmas
Nat.not_isPowerOfTwo_zero : ¬Nat.isPowerOfTwo 0
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.basicOpen_add_le : ∀ (X : AlgebraicGeometry.Scheme) {U : X.Opens} (f g : ↑(X.presheaf.obj (Opposite.op U))),
  X.basicOpen (f + g) ≤ X.basicOpen f ⊔ X.basicOpen g
-- Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Asymptotics.isEquivalent_iff_exists_eq_mul : ∀ {α : Type u_1} {β : Type u_2} [inst : NormedField β] {u v : α → β} {l : Filter α},
  Asymptotics.IsEquivalent l u v ↔ ∃ φ, ∃ (_ : Filter.Tendsto φ l (nhds 1)), u =ᶠ[l] φ * v
-- Init.Data.SInt.Basic
ISize.ofUSize.sizeOf_spec : ∀ (toUSize : USize), sizeOf { toUSize := toUSize } = 1 + sizeOf toUSize
-- Init.Grind.AC
Lean.Grind.AC.Seq.union_k.eq_1 : ∀ (s₁ s₂ : Lean.Grind.AC.Seq), s₁.union_k s₂ = Lean.Grind.AC.Seq.unionFuel_k Lean.Grind.AC.hugeFuel s₁ s₂
-- Mathlib.Algebra.Algebra.Defs
/-- This is just a special case of the global `mul_smul_comm` lemma that requires less typeclass
search (and was here first).  -/
Algebra.mul_smul_comm : ∀ {R : Type u} {A : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (s : R) (x y : A),
  x * s • y = s • (x * y)
-- Mathlib.LinearAlgebra.TensorProduct.Vanishing
/-- Converse of `TensorProduct.vanishesTrivially_of_sum_tmul_eq_zero_of_rTensor_injective`.

Assume that every expression $\sum_i m_i \otimes n_i$ which vanishes also vanishes trivially.
Then, for every submodule $M' \subseteq M$, the map $M' \otimes N \to M \otimes N$ is injective.  -/
TensorProduct.rTensor_injective_of_forall_vanishesTrivially : ∀ (R : Type u_1) [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {N : Type u_3}
  [inst_3 : AddCommGroup N] [inst_4 : Module R N],
  (∀ {l : ℕ} {m : Fin l → M} {n : Fin l → N}, ∑ i, m i ⊗ₜ[R] n i = 0 → TensorProduct.VanishesTrivially R m n) →
    ∀ (M' : Submodule R M), Function.Injective ⇑(LinearMap.rTensor N M'.subtype)
-- Mathlib.MeasureTheory.Measure.ProbabilityMeasure
/-- Normalize a finite measure so that it becomes a probability measure, i.e., divide by the
total mass.  -/
MeasureTheory.FiniteMeasure.normalize : {Ω : Type u_1} →
  [Nonempty Ω] → {m0 : MeasurableSpace Ω} → MeasureTheory.FiniteMeasure Ω → MeasureTheory.ProbabilityMeasure Ω
-- Init.Data.UInt.Lemmas
UInt16.toUInt8_ofNatTruncate_of_lt : ∀ {n : ℕ}, n < UInt16.size → (UInt16.ofNatClamp n).toUInt8 = UInt8.ofNat n
-- Mathlib.Data.Multiset.Find
/-- If two predicates agree on all the elements, so does `find?`.  -/
Multiset.find?_congr : ∀ {α : Type u_1} {p₁ p₂ : α → Prop} [inst : DecidablePred p₁] [inst_1 : DecidablePred p₂] {s : Multiset α}
  (hp₁ : {x | x ∈ s ∧ p₁ x}.Subsingleton) (h : ∀ x ∈ s, p₁ x ↔ p₂ x), Multiset.find? p₁ s hp₁ = Multiset.find? p₂ s ⋯
-- Mathlib.NumberTheory.Divisors
Int.mem_divisors_iff_natAbs_mem_divisors_natAbs : ∀ {x z : ℤ}, x ∈ z.divisors ↔ x.natAbs ∈ z.natAbs.divisors
-- Mathlib.CategoryTheory.Limits.Preserves.BifunctorCokernel
CategoryTheory.Limits.CokernelCofork.map.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  {X Y : C} {f : X ⟶ Y} (c c_1 : CategoryTheory.Limits.CokernelCofork f),
  c = c_1 → ∀ (G : CategoryTheory.Functor C D) [inst_4 : G.PreservesZeroMorphisms], c.map G = c_1.map G
-- Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
IncidenceAlgebra.mk.injEq : ∀ {𝕜 : Type u_7} {α : Type u_8} [inst : Zero 𝕜] [inst_1 : LE α] (toFun : α → α → 𝕜)
  (eq_zero_of_not_le' : ∀ ⦃a b : α⦄, ¬a ≤ b → toFun a b = 0) (toFun_1 : α → α → 𝕜)
  (eq_zero_of_not_le'_1 : ∀ ⦃a b : α⦄, ¬a ≤ b → toFun_1 a b = 0),
  ({ toFun := toFun, eq_zero_of_not_le' := eq_zero_of_not_le' } =
      { toFun := toFun_1, eq_zero_of_not_le' := eq_zero_of_not_le'_1 }) =
    (toFun = toFun_1)
-- Mathlib.Data.Set.Prod
Set.univ_pi_empty : ∀ {ι : Type u_1} {α : ι → Type u_2} [h : Nonempty ι], (Set.univ.pi fun x => ∅) = ∅
-- Mathlib.CategoryTheory.Monoidal.CommGrp_
CategoryTheory.Functor.mapCommGrpIdIso_inv_app_hom_hom_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X : CategoryTheory.CommGrp C),
  (CategoryTheory.Functor.mapCommGrpIdIso.inv.app X).hom.hom.hom = CategoryTheory.CategoryStruct.id X.X
-- Mathlib.RingTheory.Extension.Presentation.Basic
/-- The pre-images constructed in `compRelationAux` are indeed pre-images under `aux`.  -/
_private.Mathlib.RingTheory.Extension.Presentation.Basic.0.Algebra.Presentation.compRelationAux_map : ∀ {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  {ι' : Type u_1} {σ' : Type u_2} {T : Type u_3} [inst_3 : CommRing T] [inst_4 : Algebra S T]
  (Q : Algebra.Presentation S T ι' σ') (P : Algebra.Presentation R S ι σ) (r : σ'),
  (Algebra.Presentation.aux✝ Q P) (Q.compRelationAux P r) = Q.relation r
-- Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
CochainComplex.mappingCone.map.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {K₁ L₁ K₂ L₂ : CochainComplex C ℤ} (φ₁ : K₁ ⟶ L₁)
  (φ₂ : K₂ ⟶ L₂) (a : K₁ ⟶ K₂) (b : L₁ ⟶ L₂)
  (comm : CategoryTheory.CategoryStruct.comp φ₁ b = CategoryTheory.CategoryStruct.comp a φ₂),
  CochainComplex.mappingCone.map φ₁ φ₂ a b comm =
    CochainComplex.mappingCone.desc φ₁
      ((CochainComplex.HomComplex.Cochain.ofHom a).comp (CochainComplex.mappingCone.inl φ₂)
        CochainComplex.mappingCone.mapOfHomotopy._proof_2)
      (CategoryTheory.CategoryStruct.comp b (CochainComplex.mappingCone.inr φ₂)) ⋯
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
IntermediateField.bot_eq_top_of_finrank_adjoin_eq_one : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E],
  (∀ (x : E), Module.finrank F ↥F⟮x⟯ = 1) → ⊥ = ⊤
-- Mathlib.Order.Basic
lt_imp_lt_of_le_imp_le : ∀ {α : Type u_2} {β : Type u_5} [inst : LinearOrder α] [inst_1 : Preorder β] {a b : α} {c d : β},
  (a ≤ b → c ≤ d) → d < c → b < a
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.infinitesimal_iff : ∀ {x : ℝ*}, x.Infinitesimal ↔ 0 < ArchimedeanClass.mk x
-- Mathlib.CategoryTheory.Limits.HasLimits
/-- `C` has all colimits of size `v₁ u₁` (`HasColimitsOfSize.{v₁ u₁} C`)
if it has colimits of every shape `J : Type u₁` with `[Category.{v₁} J]`.
 -/
CategoryTheory.Limits.HasColimitsOfSize : (C : Type u) → [CategoryTheory.Category.{v, u} C] → Prop
-- Mathlib.Order.Interval.Multiset
Multiset.Ici.eq_1 : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrderTop α] (a : α), Multiset.Ici a = (Finset.Ici a).val
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Real.closedBall_zero_eq_Icc : ∀ (r : ℝ), Metric.closedBall 0 r = Set.Icc (-r) r
-- Mathlib.Data.Real.ConjExponents
Real.HolderTriple.one_div_ne_zero : ∀ {p q r : ℝ}, p.HolderTriple q r → 1 / p ≠ 0
-- Init.Data.SInt.Lemmas
Int16.toNatClampNeg_ofIntTruncate_of_lt : ∀ {n : ℤ}, n < 2 ^ 15 → (Int16.ofIntClamp n).toNatClampNeg = n.toNat