mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Triangulated.Orthogonal
CategoryTheory.ObjectProperty.instIsStableUnderShiftRightOrthogonal : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) {M : Type u_1}
  [inst_1 : AddGroup M] [inst_2 : CategoryTheory.HasShift C M] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C]
  [P.IsStableUnderShift M], P.rightOrthogonal.IsStableUnderShift M
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.reflection_dualMap_eq_coreflection : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) (i : ι),
  ↑(P.reflection i).dualMap ∘ₗ P.flip = P.flip ∘ₗ ↑(P.coreflection i)
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.inr_mul_inr : ∀ (R : Type u) {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Module Rᵐᵒᵖ M] (m₁ m₂ : M), TrivSqZeroExt.inr m₁ * TrivSqZeroExt.inr m₂ = 0
-- Mathlib.Topology.PartialHomeomorph.Defs
PartialHomeomorph.symm_symm : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (e : PartialHomeomorph X Y),
  e.symm.symm = e
-- Init.Data.Int.Linear
Int.Internal.Linear.Expr.eq_of_norm_eq : ∀ (ctx : Int.Internal.Linear.Context) (e : Int.Internal.Linear.Expr) (p : Int.Internal.Linear.Poly),
  e.norm.beq' p = true → Int.Internal.Linear.Expr.denote ctx e = Int.Internal.Linear.Poly.denote' ctx p
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
edist_dist : ∀ {α : Type u} [inst : PseudoMetricSpace α] (x y : α), edist x y = ENNReal.ofReal (dist x y)
-- Mathlib.Topology.Convenient.Category
/-- The adjunction between the categories `GeneratedByTopCat X` and `TopCat`.
The left adjoint is the inclusion functor, and the right adjoint sends
a topological space `Y` to the underlying type of `Y` endowed with
the `X`-generated topology.  -/
GeneratedByTopCat.adj : {ι : Type t} →
  {X : ι → Type u} → [inst : (i : ι) → TopologicalSpace (X i)] → GeneratedByTopCat.toTopCat ⊣ TopCat.toGeneratedByTopCat
-- Mathlib.RingTheory.NonUnitalSubring.Basic
/-- The image under a ring homomorphism of the `NonUnitalSubring` generated by a set equals
the `NonUnitalSubring` generated by the image of the set.  -/
NonUnitalRingHom.map_closure : ∀ {R : Type u} {S : Type v} [inst : NonUnitalNonAssocRing R] [inst_1 : NonUnitalNonAssocRing S] (f : R →ₙ+* S)
  (s : Set R), NonUnitalSubring.map f (NonUnitalSubring.closure s) = NonUnitalSubring.closure (⇑f '' s)
-- Mathlib.Algebra.SkewPolynomial.Basic
/-- `coeff p n` is the coefficient of `X ^ n` in `p`.  -/
SkewPolynomial.coeff : {R : Type u_1} → [inst : Semiring R] → SkewPolynomial R → ℕ → R
-- Mathlib.Algebra.Group.Submonoid.MulOpposite
Submonoid.op_iInf : ∀ {ι : Sort u_1} {M : Type u_2} [inst : MulOneClass M] (S : ι → Submonoid M), (iInf S).op = ⨅ i, (S i).op
-- Mathlib.Data.Finset.Defs
Finset.instUsesSetNotationForOrder : (α : Type u_4) → UsesSetNotationForOrder (Finset α)
-- Mathlib.Data.Set.Card.Arithmetic
Set.Infinite.exists_union_disjoint_cardinal_eq_of_infinite : ∀ {α : Type u_1} {s : Set α}, s.Infinite → ∃ t u, t ∪ u = s ∧ Disjoint t u ∧ Cardinal.mk ↑t = Cardinal.mk ↑u
-- Mathlib.GroupTheory.SpecificGroups.Alternating
alternatingGroup.eq_1 : ∀ (α : Type u_1) [inst : Fintype α] [inst_1 : DecidableEq α], alternatingGroup α = Equiv.Perm.sign.ker
-- Mathlib.RingTheory.NonUnitalSubring.Defs
NonUnitalSubring.toAddSubgroup_strictMono : ∀ {R : Type u} [inst : NonUnitalNonAssocRing R], StrictMono NonUnitalSubring.toAddSubgroup
-- Mathlib.Analysis.InnerProductSpace.Completion
UniformSpace.Completion.inner_coe : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (a b : E), inner 𝕜 ↑a ↑b = inner 𝕜 a b
-- Mathlib.CategoryTheory.Groupoid.Grpd.Basic
CategoryTheory.Grpd.str' : (C : CategoryTheory.Grpd) → CategoryTheory.Groupoid ↑C
-- Mathlib.Algebra.Star.Subsemiring
StarSubsemiring.mem_toSubsemiring : ∀ {R : Type v} [inst : NonAssocSemiring R] [inst_1 : StarRing R] {S : StarSubsemiring R} {x : R},
  x ∈ S.toSubsemiring ↔ x ∈ S
-- Mathlib.Data.Set.Defs
/-- A set is a collection of elements of some type `α`.

Although `Set` is defined as `α → Prop`, this is an implementation detail which should not be
relied on. Instead, `Set.ofPred` (also written `{x | p x}`) and membership of a set (`∈`) should be
used to convert between sets and predicates.
 -/
Set : Type u → Type u
-- Mathlib.Tactic.LinearCombination.Lemmas
Mathlib.Tactic.LinearCombination.smul_le_const : ∀ {α : Type u_1} {K : Type u_2} {t s : K} [inst : Ring K] [inst_1 : PartialOrder K] [IsOrderedRing K]
  [inst_3 : AddCommGroup α] [inst_4 : PartialOrder α] [IsOrderedAddMonoid α] [inst_6 : Module K α]
  [IsOrderedModule K α], t ≤ s → ∀ {a : α}, 0 ≤ a → t • a ≤ s • a
-- Mathlib.RingTheory.Regular.RegularSequence
RingTheory.Sequence.isWeaklyRegular_iff_Fin : ∀ {R : Type u_1} (M : Type u_3) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (rs : List R),
  RingTheory.Sequence.IsWeaklyRegular M rs ↔
    ∀ (i : Fin rs.length), IsSMulRegular (M ⧸ Ideal.ofList (List.take (↑i) rs) • ⊤) rs[i]
-- Mathlib.CategoryTheory.IsoCat
/-- Promotes an equivalence of categories `e : C ≌ D` whose unit and counit isomorphisms are
given by equalities of objects into an `IsoCat C D`.  -/
CategoryTheory.Equivalence.toIsoCat : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        (e : C ≌ D) →
          (h : ∀ (X : C), e.inverse.obj (e.functor.obj X) = X) →
            (h' : ∀ (Y : D), e.functor.obj (e.inverse.obj Y) = Y) →
              autoParam (∀ (X : C), e.unitIso.hom.app X = CategoryTheory.eqToHom ⋯)
                  CategoryTheory.Equivalence.toIsoCat._auto_1 →
                autoParam (∀ (Y : D), e.counitIso.hom.app Y = CategoryTheory.eqToHom ⋯)
                    CategoryTheory.Equivalence.toIsoCat._auto_3 →
                  CategoryTheory.IsoCat C D
-- Mathlib.LinearAlgebra.Matrix.DotProduct
dotProduct_eq_zero : ∀ {n : Type u_2} {R : Type u_4} [inst : Semiring R] [inst_1 : Fintype n] (v : n → R),
  (∀ (w : n → R), v ⬝ᵥ w = 0) → v = 0
-- Mathlib.MeasureTheory.Integral.Lebesgue.Add
MeasureTheory.lintegral_mul_const_le : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (r : ENNReal) (f : α → ENNReal),
  (∫⁻ (a : α), f a ∂μ) * r ≤ ∫⁻ (a : α), f a * r ∂μ
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.get?_map : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} {γ : α → Type w} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {f : (a : α) → β a → γ a} {k : α},
  (Std.DTreeMap.map f t).get? k = Option.map (f k) (t.get? k)
-- Mathlib.Order.Interval.Set.Fin
Fin.preimage_succ_Iic_succ : ∀ {n : ℕ} (i : Fin n), Fin.succ ⁻¹' Set.Iic i.succ = Set.Iic i
-- Mathlib.Algebra.Regular.Prod
Prod.isRightRegular_mk : ∀ {R : Type u_2} {S : Type u_3} [inst : Mul R] [inst_1 : Mul S] {a : R} {b : S},
  IsRightRegular (a, b) ↔ IsRightRegular a ∧ IsRightRegular b
-- Mathlib.Tactic.FunProp.Decl
Mathlib.Meta.FunProp.FunPropDecls.mk.sizeOf_spec : ∀ (decls : Lean.Meta.DiscrTree Mathlib.Meta.FunProp.FunPropDecl), sizeOf { decls := decls } = 1 + sizeOf decls
-- Mathlib.Order.Interval.Set.Basic
Set.Iic_sdiff_Iio_same : ∀ {α : Type u_1} [inst : PartialOrder α] {a : α}, Set.Iic a \ Set.Iio a = {a}
-- Mathlib.Algebra.Ring.Defs
/-- A non-unital commutative ring is a `NonUnitalRing` with commutative multiplication.  -/
NonUnitalCommRing : Type u → Type u
-- Mathlib.AlgebraicTopology.SimplicialObject.Split
CategoryTheory.SimplicialObject.Splitting.cofan.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : CategoryTheory.SimplicialObject C} (s : X.Splitting)
  (Δ : SimplexCategoryᵒᵖ),
  s.cofan Δ =
    CategoryTheory.Limits.Cofan.mk (X.obj Δ) fun A =>
      CategoryTheory.CategoryStruct.comp (s.ι (Opposite.unop A.fst).len) (X.map A.e.op)
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.nontrivial_iff : ∀ {V : Type u}, Nontrivial (SimpleGraph V) ↔ Nontrivial V
-- Mathlib.Algebra.GCDMonoid.Basic
associated_gcd_left_iff : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : GCDMonoid α] {x y : α}, Associated x (gcd x y) ↔ x ∣ y
-- Mathlib.Computability.AkraBazzi.SumTransform
AkraBazziRecurrence.mk.injEq : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : Nonempty α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ} (n₀ : ℕ)
  (n₀_gt_zero : 0 < n₀) (a_pos : ∀ (i : α), 0 < a i) (b_pos : ∀ (i : α), 0 < b i) (b_lt_one : ∀ (i : α), b i < 1)
  (g_nonneg : ∀ x ≥ 0, 0 ≤ g x) (g_grows_poly : AkraBazziRecurrence.GrowsPolynomially g)
  (h_rec : ∀ (n : ℕ), n₀ ≤ n → T n = ∑ i, a i * T (r i n) + g ↑n) (T_gt_zero' : ∀ n < n₀, 0 < T n)
  (r_lt_n : ∀ (i : α) (n : ℕ), n₀ ≤ n → r i n < n)
  (dist_r_b : ∀ (i : α), (fun n => ↑(r i n) - b i * ↑n) =o[Filter.atTop] fun n => ↑n / Real.log ↑n ^ 2) (n₀_1 : ℕ)
  (n₀_gt_zero_1 : 0 < n₀_1) (a_pos_1 : ∀ (i : α), 0 < a i) (b_pos_1 : ∀ (i : α), 0 < b i)
  (b_lt_one_1 : ∀ (i : α), b i < 1) (g_nonneg_1 : ∀ x ≥ 0, 0 ≤ g x)
  (g_grows_poly_1 : AkraBazziRecurrence.GrowsPolynomially g)
  (h_rec_1 : ∀ (n : ℕ), n₀_1 ≤ n → T n = ∑ i, a i * T (r i n) + g ↑n) (T_gt_zero'_1 : ∀ n < n₀_1, 0 < T n)
  (r_lt_n_1 : ∀ (i : α) (n : ℕ), n₀_1 ≤ n → r i n < n)
  (dist_r_b_1 : ∀ (i : α), (fun n => ↑(r i n) - b i * ↑n) =o[Filter.atTop] fun n => ↑n / Real.log ↑n ^ 2),
  ({ n₀ := n₀, n₀_gt_zero := n₀_gt_zero, a_pos := a_pos, b_pos := b_pos, b_lt_one := b_lt_one, g_nonneg := g_nonneg,
        g_grows_poly := g_grows_poly, h_rec := h_rec, T_gt_zero' := T_gt_zero', r_lt_n := r_lt_n,
        dist_r_b := dist_r_b } =
      { n₀ := n₀_1, n₀_gt_zero := n₀_gt_zero_1, a_pos := a_pos_1, b_pos := b_pos_1, b_lt_one := b_lt_one_1,
        g_nonneg := g_nonneg_1, g_grows_poly := g_grows_poly_1, h_rec := h_rec_1, T_gt_zero' := T_gt_zero'_1,
        r_lt_n := r_lt_n_1, dist_r_b := dist_r_b_1 }) =
    (n₀ = n₀_1)
-- Mathlib.Analysis.BoxIntegral.UnitPartition
BoxIntegral.unitPartition.box.upper_sub_lower : ∀ {ι : Type u_1} (n : ℕ) [inst : NeZero n] (ν : ι → ℤ) (i : ι),
  (BoxIntegral.unitPartition.box n ν).upper i - (BoxIntegral.unitPartition.box n ν).lower i = 1 / ↑n
-- Mathlib.Algebra.Lie.Subalgebra
LieSubalgebra.instIsNoetherianSubtypeMem : ∀ (R : Type u) (L : Type v) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (L' : LieSubalgebra R L)
  [IsNoetherian R L], IsNoetherian R ↥L'
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Matrix.separatingRight_toLinearMap₂'_iff : ∀ {R : Type u_1} {n : Type u_11} {m : Type u_12} [inst : CommRing R] [inst_1 : DecidableEq m] [inst_2 : Fintype m]
  [inst_3 : DecidableEq n] [inst_4 : Fintype n] {M : Matrix m n R},
  ((Matrix.toLinearMap₂' R) M).SeparatingRight ↔ M.SeparatingRight
-- Mathlib.Analysis.RCLike.Basic
RCLike.ofReal_one : ∀ {K : Type u_1} [inst : RCLike K], ↑1 = 1
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.size_inter_le_size_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → (m₁ ∩ m₂).size ≤ m₂.size
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.PUnit
FundamentalGroupoid.punitEquivDiscretePUnit_inverse : FundamentalGroupoid.punitEquivDiscretePUnit.inverse =
  (CategoryTheory.Functor.const (CategoryTheory.Discrete PUnit.{v + 1})).obj { as := PUnit.unit }
-- Mathlib.MeasureTheory.VectorMeasure.Integral
MeasureTheory.VectorMeasure.integral_neg_vectorMeasure : ∀ {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G]
  [inst_5 : NormedSpace ℝ G] {f : X → E} {μ : MeasureTheory.VectorMeasure X F} {B : E →L[ℝ] F →L[ℝ] G},
  ∫ᵛ (x : X), f x ∂[B; -μ] = -∫ᵛ (x : X), f x ∂[B; μ]
-- Mathlib.CategoryTheory.Bicategory.CatEnriched
/-- A 2-cell in `CatEnriched C` can be "made" into a 2-cell in `CatEnrichedOrdinary C`.  -/
CategoryTheory.CatEnrichedOrdinary.Hom.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.EnrichedOrdinaryCategory CategoryTheory.Cat C] →
      {X Y : CategoryTheory.CatEnrichedOrdinary C} →
        {f g : X ⟶ Y} →
          (CategoryTheory.CatEnrichedOrdinary.homEquiv f ⟶ CategoryTheory.CatEnrichedOrdinary.homEquiv g) → (f ⟶ g)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Cat
CategoryTheory.Monoidal.whiskerRight_snd : ∀ {A B : CategoryTheory.Cat} (f : A ⟶ B) (X : CategoryTheory.Cat),
  (CategoryTheory.MonoidalCategoryStruct.whiskerRight f X).toFunctor.comp (CategoryTheory.Prod.snd ↑B ↑X) =
    CategoryTheory.Prod.snd ↑A ↑X
-- Mathlib.Order.SupClosed
InfClosed.codirectedOn : ∀ {α : Type u_3} [inst : SemilatticeInf α] {s : Set α}, InfClosed s → DirectedOn (fun x1 x2 => x2 ≤ x1) s
-- Mathlib.Algebra.Category.Grp.Limits
CommGrpCat.forget₂CommMon_preservesLimitsAux.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J CommGrpCat)
  [inst_1 : Small.{u, max u v} ↑(F.comp (CategoryTheory.forget CommGrpCat)).sections],
  CommGrpCat.forget₂CommMon_preservesLimitsAux F =
    CommMonCat.limitConeIsLimit (F.comp (CategoryTheory.forget₂ CommGrpCat CommMonCat))
-- Mathlib.CategoryTheory.EquivalenceRelation
CategoryTheory.TransitiveRelation.transitivity₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {R X : C} {p₁ p₂ : R ⟶ X}
  (self : CategoryTheory.TransitiveRelation p₁ p₂),
  CategoryTheory.CategoryStruct.comp self.t p₁ = CategoryTheory.CategoryStruct.comp self.c.fst p₁
-- Mathlib.Data.List.Infix
List.decidableInfix : {α : Type u_1} → [DecidableEq α] → (l₁ l₂ : List α) → Decidable (l₁ <:+: l₂)
-- Mathlib.CategoryTheory.Retract
/-- If `X` is a retract of `Y`, then for any natural transformation `τ`,
the natural transformation `τ.app X` is a retract of `τ.app Y`.  -/
CategoryTheory.NatTrans.retractArrowApp : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u'} →
      [inst_1 : CategoryTheory.Category.{v', u'} D] →
        {F G : CategoryTheory.Functor C D} →
          (τ : F ⟶ G) → {X Y : C} → CategoryTheory.Retract X Y → CategoryTheory.RetractArrow (τ.app X) (τ.app Y)
-- Std.Http.Data.Body.Length
/-- Indicates that the HTTP message body uses **chunked transfer encoding**.
 -/
Std.Http.Body.Length.chunked : Std.Http.Body.Length
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.RingEqCnstrProof.cancelDen.inj : ∀ {c : Lean.Meta.Grind.Arith.Linear.RingEqCnstr} {val : ℤ} {x n : Lean.Grind.Linarith.Var}
  {c_1 : Lean.Meta.Grind.Arith.Linear.RingEqCnstr} {val_1 : ℤ} {x_1 n_1 : Lean.Grind.Linarith.Var},
  Lean.Meta.Grind.Arith.Linear.RingEqCnstrProof.cancelDen c val x n =
      Lean.Meta.Grind.Arith.Linear.RingEqCnstrProof.cancelDen c_1 val_1 x_1 n_1 →
    c = c_1 ∧ val = val_1 ∧ x = x_1 ∧ n = n_1
-- Batteries.Data.List.Perm
List.Perm.inter_left : ∀ {α : Type u_1} {t₁ t₂ : List α} [inst : BEq α] [LawfulBEq α] (l : List α), t₁.Perm t₂ → l ∩ t₁ = l ∩ t₂
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.size_inter_le_size_right : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → (t₁ ∩ t₂).size ≤ t₂.size
-- Mathlib.LinearAlgebra.Charpoly.Basic
LinearMap.minpoly_dvd_charpoly : ∀ {K : Type u} {M : Type v} [inst : Field K] [inst_1 : AddCommGroup M] [inst_2 : Module K M]
  [inst_3 : FiniteDimensional K M] (f : M →ₗ[K] M), minpoly K f ∣ f.charpoly
-- Mathlib.Order.RelClasses
IsWellOrder.toTrichotomous : ∀ {α : Type u} {r : α → α → Prop} [self : IsWellOrder α r], Std.Trichotomous r
-- Lean.Elab.Tactic.Simp
Lean.Elab.Tactic.instTypeNameUnusedSimpArgsInfo : TypeName Lean.Elab.Tactic.UnusedSimpArgsInfo
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.prod_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : CommMonoid β]
  [inst_3 : ContinuousMul β] {ι : Type u_3} (s : Finset ι) (f : ι → C(α, β)) (a : α),
  (∏ i ∈ s, f i) a = ∏ i ∈ s, (f i) a
-- Mathlib.AlgebraicGeometry.Artinian
AlgebraicGeometry.instIsLocallyArtinianOfIsEmptyCarrierCarrierCommRingCat : ∀ {X : AlgebraicGeometry.Scheme} [IsEmpty ↥X], AlgebraicGeometry.IsLocallyArtinian X
-- Mathlib.RingTheory.Multiplicity
multiplicity_eq_one_of_not_finiteMultiplicity : ∀ {α : Type u_1} [inst : Monoid α] {a b : α}, ¬FiniteMultiplicity a b → multiplicity a b = 1
-- Mathlib.Data.Num.Lemmas
Num.cast_bit0 : ∀ {α : Type u_1} [inst : NonAssocSemiring α] (n : Num), ↑n.bit0 = 2 * ↑n
-- Mathlib.CategoryTheory.Monoidal.Action.Opposites
CategoryTheory.MonoidalCategory.MonoidalRightAction.oppositeRightAction_actionRight_op : ∀ (C : Type u_1) (D : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : CategoryTheory.Category.{v_2, u_2} D]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D] (d : D) {c c' : C} (f : c ⟶ c'),
  CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight (Opposite.op d) f.op =
    Opposite.op (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight d f)
-- Mathlib.CategoryTheory.Localization.Monoidal.Basic
CategoryTheory.Localization.Monoidal.whiskerLeft_comp_assoc : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (L : CategoryTheory.Functor C D)
  (W : CategoryTheory.MorphismProperty C) [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : W.IsMonoidal]
  [inst_4 : L.IsLocalization W] {unit : D} (ε : L.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ≅ unit)
  (Q : CategoryTheory.LocalizedMonoidal L W ε) {X Y Z : CategoryTheory.LocalizedMonoidal L W ε} (f : X ⟶ Y) (g : Y ⟶ Z)
  {Z_1 : CategoryTheory.LocalizedMonoidal L W ε} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj Q Z ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Q (CategoryTheory.CategoryStruct.comp f g)) h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Q f)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Q g) h)
-- Mathlib.LinearAlgebra.BilinearForm.DualLattice
LinearMap.BilinForm.dualSubmodule_dualSubmodule_of_basis : ∀ {R : Type u_4} {S : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : Field S] [inst_2 : AddCommGroup M]
  [inst_3 : Algebra R S] [inst_4 : Module R M] [inst_5 : Module S M] [inst_6 : IsScalarTower R S M]
  (B : LinearMap.BilinForm S M) {ι : Type u_1} [Finite ι],
  B.Nondegenerate →
    B.IsSymm →
      ∀ (b : Module.Basis ι S M),
        B.dualSubmodule (B.dualSubmodule (Submodule.span R (Set.range ⇑b))) = Submodule.span R (Set.range ⇑b)
-- Mathlib.NumberTheory.ArithmeticFunction.Misc
ArithmeticFunction.sigma_zero_apply_prime_pow : ∀ {p i : ℕ}, Nat.Prime p → (ArithmeticFunction.sigma 0) (p ^ i) = i + 1
-- Mathlib.Algebra.Group.Submonoid.MulOpposite
AddSubmonoid.unop_eq_top : ∀ {M : Type u_2} [inst : AddZeroClass M] {S : AddSubmonoid Mᵃᵒᵖ}, S.unop = ⊤ ↔ S = ⊤
-- Mathlib.CategoryTheory.Discrete.Basic
CategoryTheory.Discrete.eqToHom.congr_simp : ∀ {α : Type u₁} {X Y : CategoryTheory.Discrete α} (h : X.as = Y.as),
  CategoryTheory.Discrete.eqToHom h = CategoryTheory.Discrete.eqToHom h
-- Mathlib.Analysis.Calculus.Deriv.Basic
derivWithin_congr_set : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {x : 𝕜} {s t : Set 𝕜}, s =ᶠ[nhds x] t → derivWithin f s x = derivWithin f t x
-- Mathlib.MeasureTheory.Integral.MeanInequalities
ENNReal.lintegral_mul_le_one_of_lintegral_rpow_eq_one : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {p q : ℝ},
  p.HolderConjugate q →
    ∀ {f g : α → ENNReal},
      AEMeasurable f μ → ∫⁻ (a : α), f a ^ p ∂μ = 1 → ∫⁻ (a : α), g a ^ q ∂μ = 1 → ∫⁻ (a : α), (f * g) a ∂μ ≤ 1
-- Init.Data.Array.Find
Array.findIdx_lt_size : ∀ {α : Type u_1} {p : α → Bool} {xs : Array α}, Array.findIdx p xs < xs.size ↔ ∃ x ∈ xs, p x = true
-- Lean.Elab.ConfigEval.Basic
Lean.Elab.ConfigEval.ConfigItem.throwInvalidOption : {α : Type} → Lean.Elab.ConfigEval.ConfigItem → Option Lean.Name → Lean.Elab.TermElabM α
-- Mathlib.CategoryTheory.Enriched.Basic
CategoryTheory.EnrichedFunctor.category_comp_out : ∀ {V : Type v} [inst : CategoryTheory.Category.{w, v} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u₁}
  [inst_2 : CategoryTheory.EnrichedCategory V C] {D : Type u₂} [inst_3 : CategoryTheory.EnrichedCategory V D]
  {X Y Z : CategoryTheory.EnrichedFunctor V C D} (F : CategoryTheory.EnrichedNatTrans X Y)
  (G : CategoryTheory.EnrichedNatTrans Y Z),
  (CategoryTheory.CategoryStruct.comp F G).out = CategoryTheory.CategoryStruct.comp F.out G.out
-- Mathlib.Combinatorics.Colex
/-- If `s ⊆ t`, then `s ≤ t` in the colex order. Note the converse does not hold, as inclusion does
not form a linear order.  -/
Finset.Colex.toColex_le_toColex_of_subset : ∀ {α : Type u_1} [inst : PartialOrder α] {s t : Finset α}, s ⊆ t → toColex s ≤ toColex t
-- Mathlib.Order.UpperLower.CompleteLattice
LowerSet.instInfSet.eq_1 : ∀ {α : Type u_1} [inst : LE α], LowerSet.instInfSet = { sInf := fun S => { carrier := ⋂ s ∈ S, ↑s, lower' := ⋯ } }
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
ContinuousMultilinearMap.piLinearEquiv_symm_apply : ∀ {ι : Type v} {M₁ : ι → Type w₁} {R' : Type u_1} {A : Type u_2} [inst : Semiring R'] [inst_1 : Semiring A]
  [inst_2 : (i : ι) → AddCommMonoid (M₁ i)] [inst_3 : (i : ι) → TopologicalSpace (M₁ i)]
  [inst_4 : (i : ι) → Module A (M₁ i)] {ι' : Type u_3} {M' : ι' → Type u_4} [inst_5 : (i : ι') → AddCommMonoid (M' i)]
  [inst_6 : (i : ι') → TopologicalSpace (M' i)] [inst_7 : ∀ (i : ι'), ContinuousAdd (M' i)]
  [inst_8 : (i : ι') → Module R' (M' i)] [inst_9 : (i : ι') → Module A (M' i)]
  [inst_10 : ∀ (i : ι'), SMulCommClass A R' (M' i)] [inst_11 : ∀ (i : ι'), ContinuousConstSMul R' (M' i)]
  (a : ContinuousMultilinearMap A M₁ ((i : ι') → M' i)) (i : ι'),
  ContinuousMultilinearMap.piLinearEquiv.symm a i = (ContinuousLinearMap.proj i).compContinuousMultilinearMap a
-- Mathlib.Order.Interval.Finset.Basic
Finset.Ico_self : ∀ {α : Type u_2} (a : α) [inst : Preorder α] [inst_1 : LocallyFiniteOrder α], Finset.Ico a a = ∅
-- Mathlib.Data.List.MinMax
List.getD_min?_eq_untopD_minimum : ∀ {α : Type u_1} [inst : LinearOrder α] (l : List α) (d : α), l.min?.getD d = WithTop.untopD d l.minimum
-- Mathlib.Algebra.Module.Torsion.Basic
Submodule.pow_pOrder_smul : ∀ {R : Type u_1} {M : Type u_2} [inst : Monoid R] [inst_1 : AddCommMonoid M] [inst_2 : DistribMulAction R M] {p : R}
  (hM : Module.IsTorsion' M ↥(Submonoid.powers p)) (x : M) [inst_3 : (n : ℕ) → Decidable (p ^ n • x = 0)],
  p ^ Submodule.pOrder hM x • x = 0
-- Mathlib.CategoryTheory.Triangulated.SpectralObject
CategoryTheory.Triangulated.SpectralObject.Hom.mk.sizeOf_spec : ∀ {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.Limits.HasZeroObject C]
  [inst_3 : CategoryTheory.HasShift C ℤ] [inst_4 : CategoryTheory.Preadditive C]
  [inst_5 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_6 : CategoryTheory.Pretriangulated C]
  {X Y : CategoryTheory.Triangulated.SpectralObject C ι} [inst_7 : SizeOf C] [inst_8 : SizeOf ι] (hom : X.ω₁ ⟶ Y.ω₁)
  (comm :
    autoParam
      (∀ {i j k : ι} (f : i ⟶ j) (g : j ⟶ k),
        CategoryTheory.CategoryStruct.comp (X.δ f g)
            ((CategoryTheory.shiftFunctor C 1).map (hom.app (CategoryTheory.ComposableArrows.mk₁ f))) =
          CategoryTheory.CategoryStruct.comp (hom.app (CategoryTheory.ComposableArrows.mk₁ g)) (Y.δ f g))
      CategoryTheory.Triangulated.SpectralObject.Hom.comm._autoParam),
  sizeOf { hom := hom, comm := comm } = 1 + sizeOf hom
-- Lean.Compiler.IR.Basic
Lean.IR.FnBody.vdecl.inj : ∀ {x : Lean.IR.VarId} {ty : Lean.IR.IRType} {e : Lean.IR.Expr} {b : Lean.IR.FnBody} {x_1 : Lean.IR.VarId}
  {ty_1 : Lean.IR.IRType} {e_1 : Lean.IR.Expr} {b_1 : Lean.IR.FnBody},
  Lean.IR.FnBody.vdecl x ty e b = Lean.IR.FnBody.vdecl x_1 ty_1 e_1 b_1 → x = x_1 ∧ ty = ty_1 ∧ e = e_1 ∧ b = b_1