mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Finsupp.Fin
/-- As a binary function, `Finsupp.cons` is injective.  -/
Finsupp.cons_injective2 : ∀ {n : ℕ} {M : Type u_1} [inst : Zero M], Function.Injective2 Finsupp.cons
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.braiding_hom_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X Y : C),
  CategoryTheory.CategoryStruct.comp (β_ X Y).hom (CategoryTheory.SemiCartesianMonoidalCategory.fst Y X) =
    CategoryTheory.SemiCartesianMonoidalCategory.snd X Y
-- Init.Grind.Config
Lean.Grind.ConfigInteractive.mk.sizeOf_spec : ∀ (toConfig : Lean.Grind.Config), sizeOf { toConfig := toConfig } = 1 + sizeOf toConfig
-- Mathlib.AlgebraicGeometry.PullbackCarrier
AlgebraicGeometry.Scheme.Pullback.residueFieldCongr_inv_residueFieldMap_ofPoint : ∀ {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} (t : ↥(CategoryTheory.Limits.pullback f g)),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.residueFieldCongr ⋯).inv
        (AlgebraicGeometry.Scheme.Hom.residueFieldMap f (AlgebraicGeometry.Scheme.Pullback.Triplet.ofPoint t).x))
      (AlgebraicGeometry.Scheme.Hom.residueFieldMap (CategoryTheory.Limits.pullback.fst f g) t) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.residueFieldCongr ⋯).inv
        (AlgebraicGeometry.Scheme.Hom.residueFieldMap g (AlgebraicGeometry.Scheme.Pullback.Triplet.ofPoint t).y))
      (AlgebraicGeometry.Scheme.Hom.residueFieldMap (CategoryTheory.Limits.pullback.snd f g) t)
-- Mathlib.CategoryTheory.Preadditive.FreydCategory.RightFreyd
/-- The fully faithful additive functor from  `V` to `RightFreyd V` sending an object `X` of `V`
to the class of the arrow `0 ⟶ X`.  -/
CategoryTheory.Preadditive.RightFreyd.functor : (V : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    [inst_1 : CategoryTheory.Preadditive V] →
      [CategoryTheory.Limits.HasZeroObject V] → CategoryTheory.Functor V (CategoryTheory.Preadditive.RightFreyd V)
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.Equiv.isEmpty_eq : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashSet.Raw α} [EquivBEq α] [LawfulHashable α],
  m₁.WF → m₂.WF → m₁.Equiv m₂ → m₁.isEmpty = m₂.isEmpty
-- Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset
Finset.prod_pos : ∀ {ι : Type u_1} {R : Type u_2} [inst : CommMonoidWithZero R] [inst_1 : PartialOrder R] [ZeroLEOneClass R]
  [PosMulStrictMono R] [Nontrivial R] {f : ι → R} {s : Finset ι}, (∀ i ∈ s, 0 < f i) → 0 < ∏ i ∈ s, f i
-- Mathlib.CategoryTheory.Monoidal.Braided.Multifunctor
CategoryTheory.BraidedCategory.Hexagon.functor₁₂₃_obj_obj_obj : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (X₁ X₂ X₃ : C),
  (((CategoryTheory.BraidedCategory.Hexagon.functor₁₂₃ C).obj X₁).obj X₂).obj X₃ =
    CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X₁ X₂) X₃
-- Lean.Meta.Tactic.Grind.Arith.FieldNormNum
_private.Lean.Meta.Tactic.Grind.Arith.FieldNormNum.0.Lean.Meta.Grind.Arith.FieldNormNum.isMulInst : Lean.Expr → Lean.Meta.Grind.Arith.FieldNormNum.M✝ Bool
-- Lean.Meta.Sym.Simp.SimpM
Lean.Meta.Sym.Simp.getMethods : Lean.Meta.Sym.Simp.SimpM Lean.Meta.Sym.Simp.Methods
-- Init.Data.Vector.Lemmas
Vector.findSome?.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ} (f : α → Option β) (as : Vector α n),
  Vector.findSome? f as = Array.findSome? f as.toArray
-- Batteries.Data.List.Basic
/-- Tail-recursive version of `swapAt`.  -/
List.swapAtTR : {α : Type u_1} → List α → ℕ → α → α × List α
-- Mathlib.Algebra.MonoidAlgebra.Basic
/-- Nested monoid algebras can be taken in an arbitrary order.  -/
MonoidAlgebra.commAlgEquiv : (R : Type u_1) →
  {A : Type u_4} →
    {M : Type u_7} →
      {N : Type u_8} →
        [inst : CommSemiring R] →
          [inst_1 : Semiring A] →
            [inst_2 : Algebra R A] →
              [inst_3 : Monoid M] →
                [inst_4 : Monoid N] → MonoidAlgebra (MonoidAlgebra A M) N ≃ₐ[R] MonoidAlgebra (MonoidAlgebra A N) M
-- Lean.KeyedDeclsAttribute
Lean.KeyedDeclsAttribute.instInhabitedOLeanEntry.default : Lean.KeyedDeclsAttribute.OLeanEntry
-- Lean.Elab.ConfigEval.DeriveEvalConfigItem
/-- Handler is called when its key matches the configuration key exactly.
The matched key is not allowed to be `Name.anonymous`.  -/
Lean.Elab.ConfigEval.EvalConfigItemHandlerKind.exact : Lean.Elab.ConfigEval.EvalConfigItemHandlerKind
-- Mathlib.Data.Num.ZNum
ZNum.mul_to_int : ∀ (m n : ZNum), ↑(m * n) = ↑m * ↑n
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.opcyclesMapIso_inv : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (e : S₁ ≅ S₂) [inst_2 : S₁.HasRightHomology] [inst_3 : S₂.HasRightHomology],
  (CategoryTheory.ShortComplex.opcyclesMapIso e).inv = CategoryTheory.ShortComplex.opcyclesMap e.inv
-- Mathlib.Order.CompleteBooleanAlgebra
_private.Mathlib.Order.CompleteBooleanAlgebra.0.Order.Coframe.MinimalAxioms.sInf_sup_eq : ∀ {α : Type u} (s : Set α) (b : α) [inst : CompleteLattice α],
  Order.Coframe.MinimalAxioms α → sInf s ⊔ b = ⨅ a ∈ s, a ⊔ b
-- Mathlib.CategoryTheory.Monoidal.Braided.Transport
_private.Mathlib.CategoryTheory.Monoidal.Braided.Transport.0.CategoryTheory.Monoidal.termE'_ : Lean.ParserDescr
-- Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
CategoryTheory.nerve.functorOfNerveMap_nerveFunctor₂_map : ∀ {C D : Type u} [inst : CategoryTheory.SmallCategory C] [inst_1 : CategoryTheory.SmallCategory D]
  (F : CategoryTheory.Functor C D),
  CategoryTheory.nerve.functorOfNerveMap ((SSet.truncation 2).map (CategoryTheory.nerveMap F)) = F
-- Mathlib.MeasureTheory.Function.LocallyIntegrable
MeasureTheory.LocallyIntegrableOn.continuousOn_mul : ∀ {X : Type u_1} {R : Type u_8} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] {μ : MeasureTheory.Measure X}
  [OpensMeasurableSpace X] [LocallyCompactSpace X] [T2Space X] [inst_5 : NormedRing R]
  [SecondCountableTopologyEither X R] {f g : X → R} {s : Set X},
  MeasureTheory.LocallyIntegrableOn f s μ →
    ContinuousOn g s → IsLocallyClosed s → MeasureTheory.LocallyIntegrableOn (fun x => g x * f x) s μ
-- Mathlib.LinearAlgebra.Prod
LinearEquiv.skewSwap_apply : ∀ {R : Type u} {M : Type v} {N : Type u_3} [inst : Semiring R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup N]
  [inst_3 : Module R M] [inst_4 : Module R N] (x : M × N), (LinearEquiv.skewSwap R M N) x = (-x.2, x.1)
-- Init.Data.Fin.Fold
_private.Init.Data.Fin.Fold.0.Fin.foldlM_loop : ∀ {m : Type u_1 → Type u_2} {α : Type u_1} {n i : ℕ} [inst : Monad m] (f : α → Fin (n + 1) → m α) (x : α)
  (h : i < n + 1),
  Fin.foldlM.loop✝ (n + 1) f x i = do
    let x ← f x ⟨i, h⟩
    Fin.foldlM.loop✝ n (fun x j => f x j.succ) x i
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.Hom.ρ_hom.sizeOf_spec : ∀ {C : Type u} [inst : SizeOf C] (X : CategoryTheory.FreeMonoidalCategory C),
  sizeOf (CategoryTheory.FreeMonoidalCategory.Hom.ρ_hom X) = 1 + sizeOf X
-- Std.Http.Protocol.H1
/-- Completes header-phase transition by emitting header/control events, updating
reader/writer states, and requesting an application answer.
 -/
_private.Std.Http.Protocol.H1.0.Std.Http.Protocol.H1.Machine.advanceAfterHeaders : {dir : Std.Http.Protocol.H1.Direction} →
  Std.Http.Protocol.H1.Machine dir → Std.Http.Protocol.H1.Reader.State dir → Std.Http.Protocol.H1.Machine dir
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Const.RoiSlice.instToIterator : {α : Type u_1} →
  {β : Type v} →
    [inst : Ord α] →
      Std.ToIterator (Std.Slice (Std.DTreeMap.Internal.Const.RoiSliceData α β)) Id
        (Std.Iterators.Types.Map (Std.DTreeMap.Internal.Zipper α fun x => β) Id Id (fun ⦃x⦄ => monadLift) fun b =>
          pure (b.fst, b.snd))
        (α × β)
-- Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
/-- The sine zeta function, i.e. the meromorphic function of `s` which agrees
with `∑' (n : ℕ), sin (2 * π * a * n) / n ^ s` for `1 < re s`.  -/
HurwitzZeta.sinZeta : UnitAddCircle → ℂ → ℂ
-- Mathlib.Algebra.Category.ModuleCat.Semi
SemimoduleCat.hom_bijective : ∀ {R : Type u} [inst : Semiring R] {M N : SemimoduleCat R}, Function.Bijective SemimoduleCat.Hom.hom
-- Init.Grind.Ring.Envelope
Lean.Grind.Ring.OfSemiring.Q.exact : ∀ {α : Type u} [inst : Lean.Grind.Semiring α] {a b : α × α},
  Lean.Grind.Ring.OfSemiring.Q.mk a = Lean.Grind.Ring.OfSemiring.Q.mk b → Lean.Grind.Ring.OfSemiring.r α a b
-- Mathlib.CategoryTheory.Limits.MonoCoprod
_private.Mathlib.CategoryTheory.Limits.MonoCoprod.0.CategoryTheory.Limits.MonoCoprod.isColimitBinaryCofanSum.match_1.splitter : {I₁ : Type u_1} →
  {I₂ : Type u_2} →
    (motive : I₁ ⊕ I₂ → Sort u_3) →
      (i : I₁ ⊕ I₂) → ((i₁ : I₁) → motive (Sum.inl i₁)) → ((i₂ : I₂) → motive (Sum.inr i₂)) → motive i
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
CategoryTheory.Limits.PushoutCocone.ofCocone_ι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor CategoryTheory.Limits.WalkingSpan C} (t : CategoryTheory.Limits.Cocone F),
  (CategoryTheory.Limits.PushoutCocone.ofCocone t).ι =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.diagramIsoSpan F).inv t.ι
-- Mathlib.Topology.Bases
/-- In a sum space `α ⊕ β`, one can form a topological basis by taking the union of
topological bases on each of the two components.  -/
TopologicalSpace.IsTopologicalBasis.sum : ∀ {α : Type u} [t : TopologicalSpace α] {β : Type u_1} [inst : TopologicalSpace β] {s : Set (Set α)},
  TopologicalSpace.IsTopologicalBasis s →
    ∀ {t_1 : Set (Set β)},
      TopologicalSpace.IsTopologicalBasis t_1 →
        TopologicalSpace.IsTopologicalBasis ((fun u => Sum.inl '' u) '' s ∪ (fun u => Sum.inr '' u) '' t_1)
-- Mathlib.Algebra.Group.Subsemigroup.Operations
Subsemigroup.map_sup : ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] (S T : Subsemigroup M) (f : M →ₙ* N),
  Subsemigroup.map f (S ⊔ T) = Subsemigroup.map f S ⊔ Subsemigroup.map f T
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.Measure.sum_cond : ∀ {α : Type u_1} {m0 : MeasurableSpace α} (μ ν : MeasureTheory.Measure α),
  (MeasureTheory.Measure.sum fun b => bif b then μ else ν) = μ + ν
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.d₃₂_single_one_fst : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A : Rep.{u, u, u} k G} (g h : G) (a : ↑A),
  ((CategoryTheory.ConcreteCategory.hom (groupHomology.d₃₂ A)) fun₀ | (1, g, h) => a) =
    (fun₀ | (1, g * h) => a) - fun₀ | (1, g) => a
-- Init.Data.List.MapIdx
List.mapFinIdx_eq_append_iff : ∀ {α : Type u_1} {β : Type u_2} {l₁ l₂ : List β} {l : List α} {f : (i : ℕ) → α → i < l.length → β},
  l.mapFinIdx f = l₁ ++ l₂ ↔
    ∃ l₁' l₂',
      ∃ (w : l = l₁' ++ l₂'),
        (l₁'.mapFinIdx fun i a h => f i a ⋯) = l₁ ∧ (l₂'.mapFinIdx fun i a h => f (i + l₁'.length) a ⋯) = l₂
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey!_insertMany_list_of_mem : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  [inst : Inhabited α] {l : List (α × β)} {k k' : α},
  (k == k') = true →
    List.Pairwise (fun a b => (a.1 == b.1) = false) l → k ∈ List.map Prod.fst l → (m.insertMany l).getKey! k' = k
-- Mathlib.LinearAlgebra.RootSystem.Finite.G2
/-- The index of the root `3α + β` where `α` is the short root and `β` is the long root.  -/
RootPairing.EmbeddedG2.threeShortAddLong : {ι : 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) → [P.EmbeddedG2] → ι
-- Mathlib.Control.Random
/-- Generate a random value of type `α`.  -/
Random.rand : {m : Type u → Type u_1} → {g : Type} → (α : Type u) → [Random m α] → [RandomGen g] → RandGT g m α
-- Init.Data.Array.Extract
Array.extract_append_left : ∀ {α : Type u_1} {as bs : Array α}, (as ++ bs).extract 0 as.size = as.extract
-- Mathlib.Data.Seq.Defs
Stream'.Seq.mem_rec_on : ∀ {α : Type u} {C : Stream'.Seq α → Prop} {a : α} {s : Stream'.Seq α},
  a ∈ s → (∀ (b : α) (s' : Stream'.Seq α), a = b ∨ C s' → C (Stream'.Seq.cons b s')) → C s
-- Mathlib.Data.Set.Lattice.Image
Set.compl_range_subset_kernImage : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set α}, (Set.range f)ᶜ ⊆ Set.kernImage f s
-- Mathlib.Analysis.Analytic.Basic
/-- If a function admits a power series expansion at `x`, then it is the locally uniform limit of
the partial sums of this power series on the disk of convergence, i.e., `f (x + y)`
is the locally uniform limit of `p.partialSum n y` there.  -/
HasFPowerSeriesOnBall.tendstoLocallyUniformlyOn : ∀ {𝕜 : 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] {f : E → F}
  {p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal},
  HasFPowerSeriesOnBall f p x r →
    TendstoLocallyUniformlyOn (fun n y => p.partialSum n y) (fun y => f (x + y)) Filter.atTop (Metric.eball 0 r)
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.support_monomial : ∀ {R : Type u} {σ : Type u_1} {a : R} {s : σ →₀ ℕ} [inst : CommSemiring R] [h : Decidable (a = 0)],
  ((MvPolynomial.monomial s) a).support = if a = 0 then ∅ else {s}
-- Mathlib.LinearAlgebra.TensorProduct.Defs
TensorProduct.map₂_mk_top_top_eq_top : ∀ (R : Type u_1) [inst : CommSemiring R] (M : Type u_7) (N : Type u_8) [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N],
  Submodule.map₂ (TensorProduct.mk R M N) ⊤ ⊤ = ⊤
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
_private.Mathlib.CategoryTheory.Limits.Shapes.Reflexive.0.CategoryTheory.Limits.WalkingParallelPair.inclusionWalkingReflexivePair.match_3.eq_3 : ∀ (motive : (Y X : CategoryTheory.Limits.WalkingParallelPair) → (X ⟶ Y) → Sort u_1)
  (x : CategoryTheory.Limits.WalkingParallelPair)
  (h_1 :
    Unit →
      motive CategoryTheory.Limits.WalkingParallelPair.one CategoryTheory.Limits.WalkingParallelPair.zero
        CategoryTheory.Limits.WalkingParallelPairHom.left)
  (h_2 :
    Unit →
      motive CategoryTheory.Limits.WalkingParallelPair.one CategoryTheory.Limits.WalkingParallelPair.zero
        CategoryTheory.Limits.WalkingParallelPairHom.right)
  (h_3 :
    (x : CategoryTheory.Limits.WalkingParallelPair) → motive x x (CategoryTheory.Limits.WalkingParallelPairHom.id x)),
  (match x, x, CategoryTheory.Limits.WalkingParallelPairHom.id x with
    | .(CategoryTheory.Limits.WalkingParallelPair.one), .(CategoryTheory.Limits.WalkingParallelPair.zero),
      CategoryTheory.Limits.WalkingParallelPairHom.left => h_1 ()
    | .(CategoryTheory.Limits.WalkingParallelPair.one), .(CategoryTheory.Limits.WalkingParallelPair.zero),
      CategoryTheory.Limits.WalkingParallelPairHom.right => h_2 ()
    | x, .(x), CategoryTheory.Limits.WalkingParallelPairHom.id .(x) => h_3 x) =
    h_3 x
-- Mathlib.Analysis.SpecialFunctions.Complex.Circle
/-- Length of the anti-clockwise arc from `x` to `y`.  -/
Circle.angleDiff : Circle → Circle → ℝ
-- Mathlib.Topology.Algebra.Monoid
Submonoid.coe_topologicalClosure : ∀ {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : Monoid M] [inst_2 : SeparatelyContinuousMul M] (s : Submonoid M),
  ↑s.topologicalClosure = closure ↑s
-- Mathlib.NumberTheory.FLT.Basic
fermatLastTheoremFor_iff_rat : ∀ {n : ℕ}, FermatLastTheoremFor n ↔ FermatLastTheoremWith ℚ n
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.le_maxKey_of_contains : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  (hc : t.contains k = true), (cmp k (t.maxKey ⋯)).isLE = true
-- Mathlib.CategoryTheory.Limits.Shapes.Preorder.WellOrderContinuous
CategoryTheory.Functor.isWellOrderContinuous_of_iso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : PartialOrder J]
  {F G : CategoryTheory.Functor J C} (e : F ≅ G) [F.IsWellOrderContinuous], G.IsWellOrderContinuous
-- Mathlib.Probability.Moments.CovarianceBilinDual
StrongDual.norm_toLpₗ_le : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {mE : MeasurableSpace E} {μ : MeasureTheory.Measure E} {p : ENNReal}
  {𝕜 : Type u_2} [inst_1 : NontriviallyNormedField 𝕜] [inst_2 : NormedSpace 𝕜 E] [OpensMeasurableSpace E]
  (L : StrongDual 𝕜 E), ‖(StrongDual.toLpₗ μ p) L‖ ≤ ‖L‖ * (MeasureTheory.eLpNorm id p μ).toReal
-- Aesop.Forward.Match.Types
Aesop.ForwardRuleMatch.mk.injEq : ∀ (rule : Aesop.ForwardRule) («match» : Aesop.CompleteMatch) (rule_1 : Aesop.ForwardRule)
  (match_1 : Aesop.CompleteMatch),
  ({ rule := rule, «match» := «match» } = { rule := rule_1, «match» := match_1 }) = (rule = rule_1 ∧ «match» = match_1)
-- Mathlib.CategoryTheory.ObjectProperty.Orthogonal
CategoryTheory.ObjectProperty.instIsClosedUnderIsomorphismsRightOrthogonal : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (P : CategoryTheory.ObjectProperty C), P.rightOrthogonal.IsClosedUnderIsomorphisms
-- Mathlib.Algebra.Module.Torsion.Basic
Submodule.coe_torsionBySet : ∀ (R : Type u_1) (M : Type u_2) [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (s : Set R),
  ↑(Submodule.torsionBySet R M s) = ⋂ y ∈ s, ⇑(DistribSMul.toLinearMap R M y) ⁻¹' {0}
-- Mathlib.Probability.Moments.Basic
ProbabilityTheory.IndepFun.integrable_exp_mul_add : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {t : ℝ} {X Y : Ω → ℝ},
  ProbabilityTheory.IndepFun X Y μ →
    MeasureTheory.Integrable (fun ω => Real.exp (t * X ω)) μ →
      MeasureTheory.Integrable (fun ω => Real.exp (t * Y ω)) μ →
        MeasureTheory.Integrable (fun ω => Real.exp (t * (X + Y) ω)) μ
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.sin_eq_zero_iff_cos_eq : ∀ {x : ℝ}, Real.sin x = 0 ↔ Real.cos x = 1 ∨ Real.cos x = -1
-- Init.Data.String.Lemmas.Iterate
String.Slice.toList_revPositionsFrom : ∀ {s : String.Slice} {p : s.Pos}, (s.revPositionsFrom p).toList = String.Slice.Model.revPositionsFrom p
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.Infinite.eq_1 : ∀ (x : ℝ*), x.Infinite = (x.InfinitePos ∨ x.InfiniteNeg)
-- Std.Data.DHashMap.Internal.Model
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.Raw₀.eraseₘaux : {α : Type u} →
  {β : α → Type v} → [BEq α] → [Hashable α] → Std.DHashMap.Internal.Raw₀ α β → α → Std.DHashMap.Internal.Raw₀ α β
-- Mathlib.CategoryTheory.Limits.Shapes.End
CategoryTheory.Limits.multispanShapeCoend_fst : ∀ (J : Type u) [inst : CategoryTheory.Category.{v, u} J] (f : CategoryTheory.Arrow J),
  (CategoryTheory.Limits.multispanShapeCoend J).fst f = f.left
-- Std.Data.HashMap.Lemmas
Std.HashMap.get!_eq_getElem! : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [inst : Inhabited β] {a : α},
  m.get! a = m[a]!
-- Mathlib.Topology.MetricSpace.Antilipschitz
/-- Extract the constant from `hf : AntilipschitzWith K f`. This is useful, e.g.,
if `K` is given by a long formula, and we want to reuse this value.  -/
AntilipschitzWith.k : {α : Type u_1} →
  {β : Type u_2} →
    [inst : PseudoEMetricSpace α] →
      [inst_1 : PseudoEMetricSpace β] → {K : NNReal} → {f : α → β} → AntilipschitzWith K f → NNReal
-- Mathlib.Order.RelSeries
RelSeries.nonempty_of_finiteDimensional : ∀ {α : Type u_1} {r : SetRel α α} [r.FiniteDimensional], Nonempty α
-- Lean.Expr
Lean.Expr.Data.hash : Lean.Expr.Data → UInt64
-- Init.Data.String.Termination
String.Pos.remainingBytes_eq : ∀ {s : String} {p : s.Pos}, p.remainingBytes = s.utf8ByteSize - p.offset.byteIdx
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap.0.Std.Internal.optionPelim'.eq_1 : ∀ {α : Type u_1} {β : Sort u_2} (a : α) (n_2 : some a = none → β) (s_2 : (val : α) → some a = some val → β),
  Std.Internal.optionPelim'✝ (some a) n_2 s_2 = s_2 a ⋯
-- Mathlib.Probability.CondVar
ProbabilityTheory.condVar_bot : ∀ {Ω : Type u_1} {m₀ : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ],
  AEMeasurable X μ → ProbabilityTheory.condVar ⊥ X μ = fun _ω => ProbabilityTheory.variance X μ
-- Mathlib.LinearAlgebra.Projectivization.Action
Projectivization.linearEquiv_is_two_pretransitive : ∀ (K : Type u_2) (V : Type u_3) [inst : AddCommGroup V] [inst_1 : DivisionRing K] [inst_2 : Module K V],
  MulAction.IsMultiplyPretransitive (V ≃ₗ[K] V) (Projectivization K V) 2
-- Lean.Environment
Lean.Kernel.Exception.deepRecursion.sizeOf_spec : sizeOf Lean.Kernel.Exception.deepRecursion = 1
-- Mathlib.Algebra.Module.Submodule.Pointwise
Submodule.instCovariantClassSetHSMulLe : ∀ {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {S : Type u_4}
  [inst_3 : Monoid S] [inst_4 : DistribMulAction S M], CovariantClass (Set S) (Submodule R M) HSMul.hSMul LE.le
-- Mathlib.Order.Antisymmetrization
OrderHom.antisymmetrization_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (f : α →o β)
  (a : Antisymmetrization α fun x1 x2 => x1 ≤ x2), f.antisymmetrization a = Quotient.map' ⇑f ⋯ a
-- Mathlib.Geometry.Manifold.Algebra.Monoid
ContMDiffAdd.toIsManifold : ∀ {𝕜 : Type u_1} {inst : NontriviallyNormedField 𝕜} {H : Type u_2} {inst_1 : TopologicalSpace H} {E : Type u_3}
  {inst_2 : NormedAddCommGroup E} {inst_3 : NormedSpace 𝕜 E} {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞}
  {G : Type u_4} {inst_4 : Add G} {inst_5 : TopologicalSpace G} {inst_6 : ChartedSpace H G} [self : ContMDiffAdd I n G],
  IsManifold I n G
-- Mathlib.Analysis.Meromorphic.Divisor
/-- Analytic functions have non-negative divisors.  -/
MeromorphicOn.AnalyticOnNhd.divisor_nonneg : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {U : Set 𝕜} {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E}, AnalyticOnNhd 𝕜 f U → 0 ≤ MeromorphicOn.divisor f U
-- Mathlib.Order.Hom.Bounded
BotHom.sup_apply : ∀ {α : Type u_2} {β : Type u_3} [inst : Bot α] [inst_1 : SemilatticeSup β] [inst_2 : OrderBot β] (f g : BotHom α β)
  (a : α), (f ⊔ g) a = f a ⊔ g a
-- Mathlib.Algebra.Algebra.Hom
/-- This ext lemma closes trivial subgoals created when chaining heterobasic ext lemmas.  -/
Algebra.ext_id : ∀ {R : Type u} (A : Type v) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (f g : R →ₐ[R] A),
  f = g
-- Lean.Meta.MkIffOfInductiveProp
/-- Calls `cases` on `h` (assumed to be a binary product) `n` times, and returns
the resulting subgoal and the new hypotheses.
 -/
_private.Lean.Meta.MkIffOfInductiveProp.0.Lean.Meta.nCasesProd : ℕ → Lean.MVarId → Lean.FVarId → Lean.MetaM (Lean.MVarId × List Lean.FVarId)
-- Mathlib.CategoryTheory.Limits.Shapes.Products
/-- `F.mapCone c` being limiting is the same as the induced fan being limiting.  -/
CategoryTheory.Limits.Fan.isLimitMapConeEquiv : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C D) →
          {ι : Type u_1} →
            (X : ι → C) →
              (c : CategoryTheory.Limits.Fan X) →
                CategoryTheory.Limits.IsLimit (F.mapCone c) ≃
                  CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fan.mk (F.obj c.pt) fun i => F.map (c.proj i))
-- Mathlib.FieldTheory.RatFunc.AsPolynomial
RatFunc.transcendental_X : ∀ {K : Type u} [inst : CommRing K] [inst_1 : IsDomain K], Transcendental K RatFunc.X
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.StructuredArrow.ofDiagEquivalence.inverse_map_right : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] (X : T × T)
  {X_1 Y : CategoryTheory.StructuredArrow X.2 (CategoryTheory.Under.forget X.1)} (g : X_1 ⟶ Y),
  ((CategoryTheory.StructuredArrow.ofDiagEquivalence.inverse X).map g).right = CategoryTheory.Under.Hom.right g.right