mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Group.Arithmetic
Units.instMeasurableSpace : {M : Type u_4} → [inst : Monoid M] → [MeasurableSpace M] → MeasurableSpace Mˣ
-- Mathlib.Topology.UniformSpace.Defs
IsUniformEmbedding.mk : ∀ {α : Type ua} {β : Type ub} [inst : UniformSpace α] [inst_1 : UniformSpace β] {f : α → β},
  IsUniformInducing f → Function.Injective f → IsUniformEmbedding f
-- Mathlib.Data.Matrix.Diagonal
Matrix.one_apply_eq : ∀ {n : Type u_3} {α : Type v} [inst : DecidableEq n] [inst_1 : Zero α] [inst_2 : One α] (i : n), 1 i i = 1
-- Mathlib.Data.ENNReal.Operations
ENNReal.add_lt_add_iff_left : ∀ {a b c : ENNReal}, a ≠ ⊤ → (a + b < a + c ↔ b < c)
-- Mathlib.Algebra.PresentedMonoid.Basic
PresentedAddMonoid.eq_1 : ∀ {α : Type u_1} (rels : FreeAddMonoid α → FreeAddMonoid α → Prop), PresentedAddMonoid rels = (addConGen rels).Quotient
-- Mathlib.Combinatorics.Configuration
Configuration.pointCount.eq_1 : ∀ (P : Type u_1) {L : Type u_2} [inst : Membership P L] (l : L), Configuration.pointCount P l = Nat.card { p // p ∈ l }
-- Mathlib.Data.Seq.Computation
Computation.ret_orElse : ∀ {α : Type u} (a : α) (c₂ : Computation α), (Computation.pure a <|> c₂) = Computation.pure a
-- Init.Prelude
/-- The number that is strictly less than `n`.

`Fin.val` is a coercion, so any `Fin n` can be used in a position where a `Nat` is expected.
 -/
Fin.val : {n : ℕ} → Fin n → ℕ
-- Mathlib.Combinatorics.SimpleGraph.Sum
_private.Mathlib.Combinatorics.SimpleGraph.Sum.0.SimpleGraph.sum.match_1.eq_1 : ∀ {V : Type u_1} {W : Type u_2} (motive : V ⊕ W → V ⊕ W → Sort u_3) (u v : V)
  (h_1 : (u v : V) → motive (Sum.inl u) (Sum.inl v)) (h_2 : (u v : W) → motive (Sum.inr u) (Sum.inr v))
  (h_3 : (x x_1 : V ⊕ W) → motive x x_1),
  (match Sum.inl u, Sum.inl v with
    | Sum.inl u, Sum.inl v => h_1 u v
    | Sum.inr u, Sum.inr v => h_2 u v
    | x, x_1 => h_3 x x_1) =
    h_1 u v
-- Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
AlgHom.coe_mapIntegralClosure : ∀ {R : Type u_1} {A : Type u_2} {S : Type u_4} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : CommRing S]
  [inst_3 : Algebra R A] [inst_4 : Algebra R S] (f : A →ₐ[R] S) (x : ↥(integralClosure R A)),
  ↑(f.mapIntegralClosure x) = f ↑x
-- Mathlib.FieldTheory.IntermediateField.ExtendRight
IntermediateField.extendRight.isFractionRing : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (F : IntermediateField K L)
  (M : Type u_3) [inst_3 : Field M] [inst_4 : Algebra K M] [inst_5 : Algebra L M] [inst_6 : IsScalarTower K L M]
  {S : Type u_5} [inst_7 : CommRing S] [inst_8 : Algebra S ↥F] [inst_9 : Algebra S M] [inst_10 : IsScalarTower S (↥F) M]
  [IsFractionRing S ↥F], IsFractionRing S ↥(F.extendRight M)
-- Mathlib.RingTheory.NonUnitalSubring.Basic
NonUnitalSubring.sInf_toAddSubgroup : ∀ {R : Type u} [inst : NonUnitalNonAssocRing R] (s : Set (NonUnitalSubring R)),
  (sInf s).toAddSubgroup = ⨅ t ∈ s, t.toAddSubgroup
-- Std.Time.Format
/-- The leanTime24Hour format, which follows the pattern `HH:mm:ss.SSSSSSSSS` for representing time
in a 24-hour clock format. It uses the default value that can be parsed with the
notation of dates.
 -/
Std.Time.Formats.leanTime24Hour : Std.Time.GenericFormat Std.Time.Awareness.any
-- Init.Data.Option.Lemmas
Option.guard_eq_filter : ∀ {α : Type u_1} {p : α → Bool} {x : α}, Option.guard p x = Option.filter p (some x)
-- Mathlib.CategoryTheory.ObjectProperty.Shift
CategoryTheory.ObjectProperty.instCommShiftHomFunctorLiftCompιIso : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C) {A : Type u_2}
  [inst_1 : AddMonoid A] [inst_2 : CategoryTheory.HasShift C A] {E : Type u_3}
  [inst_3 : CategoryTheory.Category.{v_2, u_3} E] [inst_4 : CategoryTheory.HasShift E A]
  [inst_5 : P.IsStableUnderShift A] (F : CategoryTheory.Functor E C) (hF : ∀ (X : E), P (F.obj X))
  [inst_6 : F.CommShift A], CategoryTheory.NatTrans.CommShift (P.liftCompιIso F hF).hom A
-- Init.Data.Ord.Basic
isGE_compareOfLessAndEq : ∀ {α : Type u} [inst : LT α] [inst_1 : LE α] [inst_2 : DecidableLT α] [DecidableLE α] [inst_4 : DecidableEq α],
  (∀ {x y : α}, x ≤ y → y ≤ x → x = y) →
    (∀ {x y : α}, ¬x ≤ y ↔ y < x) →
      (∀ (x y : α), x ≤ y ∨ y ≤ x) → ∀ {x y : α}, (compareOfLessAndEq x y).isGE = true ↔ y ≤ x
-- Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing
IsDedekindDomain.FiniteAdeleRing.ext : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (K : Type u_2) [inst_2 : Field K]
  [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] {a₁ a₂ : IsDedekindDomain.FiniteAdeleRing R K},
  (∀ (v : IsDedekindDomain.HeightOneSpectrum R), a₁ v = a₂ v) → a₁ = a₂
-- Mathlib.Algebra.GroupWithZero.Defs
/-- If `α` has no zero divisors, then for elements `a, b : α`, `a * b` is nonzero iff so is
`b * a`.  -/
mul_ne_zero_comm : ∀ {M₀ : Type u_1} [inst : MulZeroClass M₀] [NoZeroDivisors M₀] {a b : M₀}, a * b ≠ 0 ↔ b * a ≠ 0
-- Mathlib.Data.Seq.Defs
Stream'.Seq.TerminatedAt.eq_1 : ∀ {α : Type u} (s : Stream'.Seq α) (n : ℕ), s.TerminatedAt n = (s.get? n = none)
-- Mathlib.Combinatorics.Matroid.Circuit
Matroid.isCircuit_iff_dep_forall_sdiff_singleton_indep : ∀ {α : Type u_1} {M : Matroid α} {C : Set α}, M.IsCircuit C ↔ M.Dep C ∧ ∀ e ∈ C, M.Indep (C \ {e})
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
/-- Type copy `Matrix m n A` meant for matrices with entries in a C⋆-algebra. This is
a C⋆-algebra when `m = n`.  -/
CStarMatrix : Type u_1 → Type u_2 → Type u_3 → Type (max u_1 u_2 u_3)
-- Mathlib.CategoryTheory.Monoidal.NaturalTransformation
CategoryTheory.LaxMonoidalFunctor.Hom.mk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.MonoidalCategory D] →
            {F G : CategoryTheory.LaxMonoidalFunctor C D} →
              (hom : F.toFunctor ⟶ G.toFunctor) →
                autoParam (CategoryTheory.NatTrans.IsMonoidal hom)
                    CategoryTheory.LaxMonoidalFunctor.Hom.isMonoidal._autoParam →
                  F.Hom G
-- Mathlib.Algebra.Group.Defs
instIsDedekindFiniteAddMonoidOfIsRightCancelAdd : ∀ (M : Type u_2) [inst : AddMonoid M] [IsRightCancelAdd M], IsDedekindFiniteAddMonoid M
-- Mathlib.Analysis.Calculus.ContDiff.Basic
iteratedFDeriv_fun_zero : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {n : ℕ},
  (iteratedFDeriv 𝕜 n fun x => 0) = 0
-- Mathlib.NumberTheory.ArithmeticFunction.Moebius
/-- Möbius inversion for functions to a `CommGroupWithZero`.  -/
ArithmeticFunction.prod_eq_iff_prod_pow_moebius_eq_of_nonzero : ∀ {R : Type u_1} [inst : CommGroupWithZero R] {f g : ℕ → R},
  (∀ (n : ℕ), 0 < n → f n ≠ 0) →
    (∀ (n : ℕ), 0 < n → g n ≠ 0) →
      ((∀ n > 0, ∏ i ∈ n.divisors, f i = g n) ↔
        ∀ n > 0, ∏ x ∈ n.divisorsAntidiagonal, g x.2 ^ ArithmeticFunction.moebius x.1 = f n)
-- Mathlib.Topology.Category.Profinite.Nobeling.Span
Profinite.NobelingProof.GoodProducts.finsuppSum_mem_span_eval : ∀ {I : Type u} (C : Set (I → Bool)) [inst : LinearOrder I] (s : Finset I) {a : I} {as : List I},
  List.IsChain (fun x1 x2 => x1 > x2) (a :: as) →
    ∀ {c : Profinite.NobelingProof.Products I →₀ ℤ},
      ↑c.support ⊆ {m | ↑m ≤ as} →
        (c.sum fun a_1 b =>
            Profinite.NobelingProof.e (Profinite.NobelingProof.π C fun x => x ∈ s) a *
              b • Profinite.NobelingProof.Products.eval (Profinite.NobelingProof.π C fun x => x ∈ s) a_1) ∈
          Submodule.span ℤ
            (Profinite.NobelingProof.Products.eval (Profinite.NobelingProof.π C fun x => x ∈ s) '' {m | ↑m ≤ a :: as})
-- Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory
CategoryTheory.FreeGroupoid.mapId_hom_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.FreeGroupoid C),
  (CategoryTheory.FreeGroupoid.mapId C).hom.app X = CategoryTheory.CategoryStruct.id X
-- Mathlib.CategoryTheory.Sites.Subsheaf
/-- Every subpresheaf of a separated presheaf is itself separated.  -/
CategoryTheory.Subfunctor.isSeparated : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor Cᵒᵖ (Type w)}
  (G : CategoryTheory.Subfunctor F) {J : CategoryTheory.GrothendieckTopology C},
  CategoryTheory.Presieve.IsSeparated J F → CategoryTheory.Presieve.IsSeparated J G.toFunctor
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Iso.isoCompInverse_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] {F : CategoryTheory.Functor C E}
  {G : CategoryTheory.Functor C D} {H : D ≌ E} (i : G.comp H.functor ≅ F) (X : C),
  i.isoCompInverse.hom.app X =
    CategoryTheory.CategoryStruct.comp (H.unitIso.hom.app (G.obj X)) (H.inverse.map (i.hom.app X))
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.quiver : {B : Type u} → [Quiver B] → Quiver (CategoryTheory.FreeBicategory B)
-- Mathlib.Topology.Compactness.Compact
/-- A set `s` is compact if and only if
for every family of closed sets whose intersection avoids `s`,
there exists a finite subfamily whose intersection avoids `s`.  -/
isCompact_iff_finite_subfamily_closed : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X},
  IsCompact s ↔
    ∀ {ι : Type u} (t : ι → Set X), (∀ (i : ι), IsClosed (t i)) → s ∩ ⋂ i, t i = ∅ → ∃ u, s ∩ ⋂ i ∈ u, t i = ∅
-- Lean.Meta.Tactic.Injection
Lean.Meta.InjectionsResult.solved.sizeOf_spec : sizeOf Lean.Meta.InjectionsResult.solved = 1
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
/-- If a function is countably sub-multiplicative then it is sub-multiplicative on finite sets  -/
rel_iSup_prod : ∀ {M : Type u_1} [inst : CommMonoid M] [inst_1 : TopologicalSpace M] {α : Type u_3} {γ : Type u_5}
  [inst_2 : CompleteLattice α] (m : α → M),
  m ⊥ = 1 →
    ∀ (R : M → M → Prop),
      (∀ (s : ℕ → α), R (m (⨆ i, s i)) (∏' (i : ℕ), m (s i))) →
        ∀ (s : γ → α) (t : Finset γ), R (m (⨆ d ∈ t, s d)) (∏ d ∈ t, m (s d))
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithTop.ofNat_ne_top : ∀ {α : Type u} [inst : AddMonoidWithOne α] (n : ℕ) [inst_1 : n.AtLeastTwo], OfNat.ofNat n ≠ ⊤
-- Mathlib.MeasureTheory.Integral.Bochner.L1
/-- Bochner integral of simple functions whose codomain is a real `NormedSpace`.
This is equal to `∑ x ∈ f.range, μ.real (f ⁻¹' {x}) • x` (see `integral_eq`).  -/
MeasureTheory.SimpleFunc.integral : {α : Type u_1} →
  {F : Type u_3} →
    [inst : NormedAddCommGroup F] →
      [NormedSpace ℝ F] → {x : MeasurableSpace α} → MeasureTheory.Measure α → MeasureTheory.SimpleFunc α F → F
-- Mathlib.Data.List.Sigma
List.map₂_keys : ∀ {α : Type u} {β : α → Type u_1} {β' : α → Type u_2} (f : (a : α) → β a → β' a) (l : List ((a : α) × β a)),
  (List.map (Sigma.map id f) l).keys = l.keys
-- Lean.Elab.Tactic.Conv.Basic
Lean.Elab.Tactic.Conv.getLhsRhsCore : Lean.MVarId → Lean.MetaM (Lean.Expr × Lean.Expr)
-- Mathlib.SetTheory.Cardinal.Regular
/-- A cardinal is inaccessible if it is an uncountable regular strong limit cardinal.  -/
Cardinal.IsInaccessible : Cardinal.{u_1} → Prop
-- Mathlib.Topology.Algebra.Group.Pointwise
IsClosed.mul_left_of_isCompact : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Group G] [IsTopologicalGroup G] {s t : Set G},
  IsClosed t → IsCompact s → IsClosed (s * t)
-- Init.Data.Order.Ord
Std.LawfulBEqOrd.lawfulEqOrd : ∀ {α : Type u} [inst : BEq α] [inst_1 : Ord α] [Std.LawfulBEqOrd α] [LawfulBEq α], Std.LawfulEqOrd α
-- Mathlib.CategoryTheory.Monoidal.Limits.Shapes.Pullback
CategoryTheory.MonoidalCategory.IsPushout.inl_isoPushout_hom_whiskerRight_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {Z X Y P : C}
  {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P} (hP : CategoryTheory.IsPushout f g inl inr)
  [inst_2 : CategoryTheory.Limits.HasPushout f g] {Q Z_1 : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.Limits.pushout f g) Q ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight inl Q)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight hP.isoPushout.hom Q) h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.pushout.inl f g) Q) h
-- Mathlib.CategoryTheory.Limits.Types.Images
CategoryTheory.Limits.Types.Image.lift_fac : ∀ {α β : Type u} {f : α ⟶ β} (F' : CategoryTheory.Limits.MonoFactorisation f),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Types.Image.lift F') F'.m =
    CategoryTheory.Limits.Types.Image.ι f
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.range_smul_range : ∀ {α : Type u_2} {β : Type u_3} {ι : Type u_5} {κ : Type u_6} [inst : SMul α β] (b : ι → α) (c : κ → β),
  Set.range b • Set.range c = Set.range fun p => b p.1 • c p.2
-- Mathlib.Analysis.SumIntegralComparisons
/-- **Integral test**: bounds the sum of a nonnegative antitone function by an integral.  -/
AntitoneOn.tsum_le_integral : ∀ {f : ℝ → ℝ},
  AntitoneOn f (Set.Ici 0) →
    MeasureTheory.IntegrableOn f (Set.Ioi 0) MeasureTheory.volume →
      (∀ t ∈ Set.Ioi 0, 0 ≤ f t) → ∑' (n : ℕ), f ↑n ≤ f 0 + ∫ (x : ℝ) in Set.Ioi 0, f x
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
CategoryTheory.WithInitial.down.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C}
  (f : CategoryTheory.WithInitial.of X ⟶ CategoryTheory.WithInitial.of Y), CategoryTheory.WithInitial.down f = f
-- Mathlib.Order.Filter.Basic
Filter.neBot_sup_of_right : ∀ {α : Type u} {f g : Filter α} [g.NeBot], (f ⊔ g).NeBot
-- Mathlib.CategoryTheory.Limits.Constructions.Over.Connected
/-- `conePost` is compatible with the forgetful functors on over categories.  -/
CategoryTheory.Over.conePostIso : {J : Type u'} →
  [inst : CategoryTheory.Category.{v', u'} J] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        (F : CategoryTheory.Functor J C) →
          (i : J) →
            (CategoryTheory.Over.conePost F i).comp
                (CategoryTheory.Limits.Cone.functoriality (CategoryTheory.Over.post F)
                  (CategoryTheory.Over.forget (F.obj i))) ≅
              CategoryTheory.Limits.Cone.whiskering (CategoryTheory.Over.forget i)
-- Init.Data.SInt.Lemmas
Int16.toUInt16_sub : ∀ (a b : Int16), (a - b).toUInt16 = a.toUInt16 - b.toUInt16
-- Init.Data.UInt.Lemmas
UInt64.toNat_div : ∀ (a b : UInt64), (a / b).toNat = a.toNat / b.toNat
-- Mathlib.NumberTheory.ArithmeticFunction.Misc
ArithmeticFunction.sum_Ioc_mul_eq_sum_prod_filter : ∀ {R : Type u_2} [inst : Semiring R] (f g : ArithmeticFunction R) (N : ℕ),
  ∑ n ∈ Finset.Ioc 0 N, (f * g) n = ∑ x ∈ Finset.Ioc 0 N ×ˢ Finset.Ioc 0 N with x.1 * x.2 ≤ N, f x.1 * g x.2
-- Mathlib.LinearAlgebra.BilinearForm.TensorProduct
/-- The tensor product of two bilinear forms injects into bilinear forms on tensor products.

Note this is heterobasic; the bilinear form on the left can take values in an (commutative) algebra
over the ring in which the right bilinear form is valued.  -/
LinearMap.BilinForm.tensorDistrib : (R : Type uR) →
  (A : Type uA) →
    {M₁ : Type uM₁} →
      {M₂ : Type uM₂} →
        [inst : CommSemiring R] →
          [inst_1 : CommSemiring A] →
            [inst_2 : AddCommMonoid M₁] →
              [inst_3 : AddCommMonoid M₂] →
                [inst_4 : Algebra R A] →
                  [inst_5 : Module R M₁] →
                    [inst_6 : Module A M₁] →
                      [inst_7 : SMulCommClass R A M₁] →
                        [IsScalarTower R A M₁] →
                          [inst_9 : Module R M₂] →
                            TensorProduct R (LinearMap.BilinForm A M₁) (LinearMap.BilinForm R M₂) →ₗ[A]
                              LinearMap.BilinForm A (TensorProduct R M₁ M₂)
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.foldlM_eq_foldlM_toArray : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} {δ : Type w} {m : Type w → Type w'} [inst : Monad m]
  [LawfulMonad m] {f : δ → α → m δ} {init : δ}, Std.TreeSet.foldlM f init t = Array.foldlM f init t.toArray
-- Mathlib.CategoryTheory.Localization.Predicate
/-- Given a localization functor `L : C ⥤ D` for `W : MorphismProperty C` and
a functor `F : C ⥤ E` which inverts `W`, this is a choice of functor
`D ⥤ E` which lifts `F`.  -/
CategoryTheory.Localization.lift : {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] →
        {W : CategoryTheory.MorphismProperty C} →
          {E : Type u_3} →
            [inst_2 : CategoryTheory.Category.{v_3, u_3} E] →
              (F : CategoryTheory.Functor C E) →
                W.IsInvertedBy F → (L : CategoryTheory.Functor C D) → [L.IsLocalization W] → CategoryTheory.Functor D E
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.toList_filter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} {f : (a : α) → β a → Bool},
  (Std.DTreeMap.filter f t).toList = List.filter (fun p => f p.fst p.snd) t.toList
-- Mathlib.Order.Category.BoolAlg
_private.Mathlib.Order.Category.BoolAlg.0.BoolAlg.Hom.mk.sizeOf_spec : ∀ {X Y : BoolAlg} (hom' : BoundedLatticeHom ↑X ↑Y), sizeOf { hom' := hom' } = 1 + sizeOf hom'
-- Init.Data.Vector.Lemmas
Vector.or_all_distrib_left : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {p : α → Bool} {q : Bool}, (q || xs.all p) = xs.all fun a => q || p a
-- Lean.Meta.ACLt
_private.Lean.Meta.ACLt.0.Lean.Meta.ACLt.main.someChildGe : Lean.Meta.ACLt.ReduceMode → Lean.Expr → Lean.Expr → Lean.MetaM Bool
-- Mathlib.Algebra.Lie.SemiDirect
LieAlgebra.SemiDirectSum.instAddCommGroup : {R : Type u_1} →
  [inst : CommRing R] →
    {K : Type u_2} →
      [inst_1 : LieRing K] →
        [inst_2 : LieAlgebra R K] →
          {L : Type u_3} →
            [inst_3 : LieRing L] →
              [inst_4 : LieAlgebra R L] → (ψ : L →ₗ⁅R⁆ LieDerivation R K K) → AddCommGroup (K ⋊⁅ψ⁆ L)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.get?_eq_of_equiv : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m₁ m₂ : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [EquivBEq α] [LawfulHashable α],
  (↑m₁).WF →
    (↑m₂).WF →
      (↑m₁).Equiv ↑m₂ →
        ∀ {k : α}, Std.DHashMap.Internal.Raw₀.Const.get? m₁ k = Std.DHashMap.Internal.Raw₀.Const.get? m₂ k
-- Std.Data.Iterators.Lemmas.Producers.Repeat
Std.Iter.step_repeat : ∀ {α : Type w} {f : α → α} {init : α},
  (Std.Iter.repeat f init).step = Std.PlausibleIterStep.yield (Std.Iter.repeat f (f init)) init ⋯
-- Mathlib.Data.Bool.Basic
Bool.and_eq_true_eq_eq_true_and_eq_true : ∀ (a b : Bool), ((a && b) = true) = (a = true ∧ b = true)
-- Mathlib.Data.Seq.Computation
Computation.get_mem : ∀ {α : Type u} (s : Computation α) [h : s.Terminates], s.get ∈ s
-- Lean.Meta.Basic
Lean.Meta.instBEqDefEqCacheKey.beq : Lean.Meta.DefEqCacheKey → Lean.Meta.DefEqCacheKey → Bool
-- Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Polynomial.IsMonicOfDegree.sub : ∀ {R : Type u_1} [inst : Ring R] {p q : Polynomial R} {n : ℕ},
  p.IsMonicOfDegree n → q.natDegree < n → (p - q).IsMonicOfDegree n
-- Init.Data.SInt.Bitwise
ISize.or_zero : ∀ {a : ISize}, a ||| 0 = a
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.getKeyLE_eq : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ t₂ : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) {k : α} {he : ∃ a ∈ t₁, (compare a k).isLE = true},
  Std.DTreeMap.Internal.Impl.getKeyLE k t₁ ⋯ he = Std.DTreeMap.Internal.Impl.getKeyLE k t₂ ⋯ ⋯
-- Mathlib.Data.ZMod.Basic
ZMod.val_ofNat_of_lt : ∀ {n a : ℕ} [inst : a.AtLeastTwo], a < n → (OfNat.ofNat a).val = OfNat.ofNat a
-- Mathlib.Order.Heyting.Basic
himp_eq_himp_iff : ∀ {α : Type u_2} [inst : GeneralizedHeytingAlgebra α] {a b : α}, b ⇨ a = a ⇨ b ↔ a = b
-- Mathlib.AlgebraicTopology.SimplicialSet.Boundary
SSet.boundary.instMonoδStdSimplex : ∀ {n : ℕ} (i : Fin (n + 2)), CategoryTheory.Mono (SSet.stdSimplex.δ i)
-- Lean.Elab.Deriving.Basic
Lean.Elab.elabDeriving : Lean.Elab.Command.CommandElab
-- Mathlib.Algebra.Polynomial.Expand
Polynomial.expand_eq_sum : ∀ {R : Type u} [inst : CommSemiring R] (p : ℕ) {f : Polynomial R},
  (Polynomial.expand R p) f = f.sum fun e a => Polynomial.C a * (Polynomial.X ^ p) ^ e
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- The angle between two nonnegative multiples of the same vector is 0.  -/
Orientation.oangle_smul_smul_self_of_nonneg : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) (x : V) {r₁ r₂ : ℝ}, 0 ≤ r₁ → 0 ≤ r₂ → o.oangle (r₁ • x) (r₂ • x) = 0
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.Exact.epi_toCycles : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S : CategoryTheory.ShortComplex C}, S.Exact → ∀ [inst_2 : S.HasLeftHomology], CategoryTheory.Epi S.toCycles
-- Std.Time.Time.Unit.Nanosecond
Std.Time.Nanosecond.instLawfulEqOrdSpan : Std.LawfulEqOrd Std.Time.Nanosecond.Span
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap.0.Std.IterM.step_filterMapWithPostcondition.match_3.eq_1 : ∀ {α β : Type u_1} {m : Type u_1 → Type u_2} [inst : Std.Iterator α m β] {it : Std.IterM m β}
  (motive : it.Step → Sort u_3) (it' : Std.IterM m β) (out : β) (h : it.IsPlausibleStep (Std.IterStep.yield it' out))
  (h_1 :
    (it' : Std.IterM m β) →
      (out : β) → (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩)
  (h_2 : (it' : Std.IterM m β) → (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩)
  (h_3 : (h : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩),
  (match ⟨Std.IterStep.yield it' out, h⟩ with
    | ⟨Std.IterStep.yield it' out, h⟩ => h_1 it' out h
    | ⟨Std.IterStep.skip it', h⟩ => h_2 it' h
    | ⟨Std.IterStep.done, h⟩ => h_3 h) =
    h_1 it' out h
-- Mathlib.Tactic.ClickSuggestions.SectionState
Mathlib.Tactic.ClickSuggestions.SectionState.mk.sizeOf_spec : ∀ {α : Type} [inst : SizeOf α] (results : Array (Mathlib.Tactic.ClickSuggestions.Result α))
  (errors : Array ProofWidgets.Html),
  sizeOf { results := results, errors := errors } = 1 + sizeOf results + sizeOf errors
-- Lean.Meta.DiscrTree.Basic
Lean.Meta.DiscrTree.insertCore : {α : Type} → [BEq α] → Lean.Meta.DiscrTree α → Array Lean.Meta.DiscrTree.Key → α → Lean.Meta.DiscrTree α
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.Goal.toGoalState : Lean.Meta.Grind.Goal → Lean.Meta.Grind.GoalState
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithTerminal.mkCommaObject_left_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  (F : CategoryTheory.Functor (CategoryTheory.WithTerminal C) D) (X : C),
  (CategoryTheory.WithTerminal.mkCommaObject F).left.obj X = F.obj (CategoryTheory.WithTerminal.incl.obj X)
-- Mathlib.Analysis.Asymptotics.TVS
Asymptotics.IsBigOTVS.refl : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} [inst : NontriviallyNormedField 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : TopologicalSpace E] [inst_3 : Module 𝕜 E] (f : α → E) (l : Filter α), f =O[𝕜; l] f
-- Init.Prelude
Lean.instInhabitedName : Inhabited Lean.Name
-- Mathlib.MeasureTheory.Function.SimpleFuncDense
MeasureTheory.SimpleFunc.approxOn_comp : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : PseudoEMetricSpace α]
  [inst_2 : OpensMeasurableSpace α] [inst_3 : MeasurableSpace β] {γ : Type u_3} [inst_4 : MeasurableSpace γ] {f : β → α}
  (hf : Measurable f) {g : γ → β} (hg : Measurable g) {s : Set α} {y₀ : α} (h₀ : y₀ ∈ s)
  [inst_5 : TopologicalSpace.SeparableSpace ↑s] (n : ℕ),
  MeasureTheory.SimpleFunc.approxOn (f ∘ g) ⋯ s y₀ h₀ n = (MeasureTheory.SimpleFunc.approxOn f hf s y₀ h₀ n).comp g hg
-- Mathlib.Order.Filter.CountablyGenerated
Filter.HasCountableBasis.toHasBasis : ∀ {α : Type u_1} {ι : Type u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α}, l.HasCountableBasis p s → l.HasBasis p s