mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
/-- If corresponding pairs of points in two angles have the same vector span, twice those angles
are equal.  -/
EuclideanGeometry.two_zsmul_oangle_of_vectorSpan_eq : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {p₁ p₂ p₃ p₄ p₅ p₆ : P},
  vectorSpan ℝ {p₁, p₂} = vectorSpan ℝ {p₄, p₅} →
    vectorSpan ℝ {p₃, p₂} = vectorSpan ℝ {p₆, p₅} →
      2 • EuclideanGeometry.oangle p₁ p₂ p₃ = 2 • EuclideanGeometry.oangle p₄ p₅ p₆
-- Mathlib.RingTheory.PrincipalIdealDomain
Submodule.IsPrincipal.mem_iff_generator_dvd : ∀ {R : Type u} [inst : CommSemiring R] (S : Ideal R) [inst_1 : Submodule.IsPrincipal S] {x : R},
  x ∈ S ↔ Submodule.IsPrincipal.generator S ∣ x
-- Mathlib.Probability.Distributions.Gaussian.Multivariate
/-- Multivariate Gaussian measure on `EuclideanSpace ℝ ι` with mean `μ` and covariance
matrix `S`. This only makes sense when `S` is positive semidefinite,
as then `CFC.sqrt S * CFC.sqrt S = S`. Otherwise `CFC.sqrt S = 0`, and
`multivariateGaussian μ S = Measure.dirac μ` (see `multivariateGaussian_of_not_posSemidef`).  -/
ProbabilityTheory.multivariateGaussian : {ι : Type u_1} →
  [Fintype ι] → [DecidableEq ι] → EuclideanSpace ℝ ι → Matrix ι ι ℝ → MeasureTheory.Measure (EuclideanSpace ℝ ι)
-- Mathlib.SetTheory.Ordinal.Basic
/-- A well order `r` is order-isomorphic to the set of ordinals smaller than `type r`.
`enum r ⟨o, h⟩` is the `o`-th element of `α` ordered by `r`.

That is, `enum` maps an initial segment of the ordinals, those less than the order type of `r`, to
the elements of `α`.  -/
Ordinal.enum : {α : Type u} → (r : α → α → Prop) → [inst : IsWellOrder α r] → (fun x1 x2 => x1 < x2) ≃r r
-- Mathlib.Algebra.Order.Hom.Monoid
OrderMonoidHom.coe_id : ∀ (α : Type u_2) [inst : Preorder α] [inst_1 : MulOneClass α], ⇑(OrderMonoidHom.id α) = id
-- Init.Core
/-- A setoid's equivalence relation is reflexive.  -/
Setoid.refl : ∀ {α : Sort u} [inst : Setoid α] (a : α), a ≈ a
-- Mathlib.Algebra.ContinuedFractions.Basic
GenContFract.instDecidableTerminatedAt : {α : Type u_1} → (g : GenContFract α) → (n : ℕ) → Decidable (g.TerminatedAt n)
-- Lean.Parser.Term
Lean.Parser.Term.hygienicLParen.formatter : Lean.PrettyPrinter.Formatter
-- Lean.Meta.Match.MatcherApp.Transform
/-- Extra equation fvars added by `addEqualities` (see `heq` in the example above).  -/
Lean.Meta.MatcherApp.TransformAltFVars.extraEqs : Lean.Meta.MatcherApp.TransformAltFVars → Array Lean.Expr
-- Mathlib.Topology.MetricSpace.Contracting
ContractingWith.one_sub_K_ne_zero : ∀ {α : Type u_1} [inst : EMetricSpace α] {K : NNReal} {f : α → α}, ContractingWith K f → 1 - ↑K ≠ 0
-- Mathlib.Algebra.Group.TypeTags.Basic
Multiplicative.ofAdd_symm_eq : ∀ {α : Type u}, Multiplicative.ofAdd.symm = Multiplicative.toAdd
-- Mathlib.Probability.Kernel.IonescuTulcea.Traj
ProbabilityTheory.Kernel.lintegral_traj₀ : ∀ {X : ℕ → Type u_1} [inst : (n : ℕ) → MeasurableSpace (X n)]
  {κ : (n : ℕ) → ProbabilityTheory.Kernel ((i : ↥(Finset.Iic n)) → X ↑i) (X (n + 1))}
  [inst_1 : ∀ (n : ℕ), ProbabilityTheory.IsMarkovKernel (κ n)] {a : ℕ} (x₀ : (i : ↥(Finset.Iic a)) → X ↑i)
  {f : ((n : ℕ) → X n) → ENNReal},
  AEMeasurable f ((ProbabilityTheory.Kernel.traj κ a) x₀) →
    ∫⁻ (x : (n : ℕ) → X n), f x ∂(ProbabilityTheory.Kernel.traj κ a) x₀ =
      ∫⁻ (x : (n : ℕ) → X n), f (Function.updateFinset x (Finset.Iic a) x₀) ∂(ProbabilityTheory.Kernel.traj κ a) x₀
-- Mathlib.Data.Set.Function
Equiv.Perm.extendDomain.congr_simp : ∀ {α' : Type u_9} {β' : Type u_10} (e e_1 : Equiv.Perm α'),
  e = e_1 →
    ∀ {p : β' → Prop} {inst : DecidablePred p} [inst_1 : DecidablePred p] (f f_1 : α' ≃ Subtype p),
      f = f_1 → e.extendDomain f = e_1.extendDomain f_1
-- Mathlib.Algebra.Homology.ShortComplex.Basic
/-- Morphisms of short complexes are the commutative diagrams of the obvious shape.  -/
CategoryTheory.ShortComplex.Hom : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      CategoryTheory.ShortComplex C → CategoryTheory.ShortComplex C → Type v_1
-- Mathlib.Algebra.Homology.ImageToKernel
imageToKernel_arrow : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {A B C : V}
  (f : A ⟶ B) [inst_2 : CategoryTheory.Limits.HasImage f] (g : B ⟶ C) [inst_3 : CategoryTheory.Limits.HasKernel g]
  (w : CategoryTheory.CategoryStruct.comp f g = 0),
  CategoryTheory.CategoryStruct.comp (imageToKernel f g w) (CategoryTheory.Limits.kernelSubobject g).arrow =
    (CategoryTheory.Limits.imageSubobject f).arrow
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getD_eq_getD_get? : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α], t.WF → ∀ {a : α} {fallback : β a}, t.getD a fallback = (t.get? a).getD fallback
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Over
CategoryTheory.Over.tensorUnit_left : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C] {X : C},
  (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over X)).left = X
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- Given a closed set `s`, a point belongs to `s` iff its infimum distance to this set vanishes.  -/
IsClosed.notMem_iff_infDist_pos : ∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α} {x : α},
  IsClosed s → s.Nonempty → (x ∉ s ↔ 0 < Metric.infDist x s)
-- Mathlib.CategoryTheory.Presentable.Finite
CategoryTheory.isFinitelyPresentable_iff_preservesFilteredColimitsOfSize : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C},
  CategoryTheory.IsFinitelyPresentable X ↔
    CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v, v, u, v + 1}
      (CategoryTheory.coyoneda.obj (Opposite.op X))
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
AlgebraicGeometry.Scheme.IdealSheafData.subschemeCover.eq_1 : ∀ {X : AlgebraicGeometry.Scheme} (I : X.IdealSheafData),
  I.subschemeCover =
    { I₀ := ↑X.affineOpens, X := fun U => CommRingCat.of (↑(X.presheaf.obj (Opposite.op ↑U)) ⧸ I.ideal U),
      f := fun U => CategoryTheory.CategoryStruct.comp (I.glueData.ι U) I.subschemeIso.inv,
      idx := fun x => AlgebraicGeometry.Scheme.Cover.idx (X.openCoverOfIsOpenCover (fun i => ↑i) ⋯) ↑x, covers := ⋯,
      map_prop := ⋯ }
-- Mathlib.Algebra.GroupWithZero.Basic
isReduced_iff : ∀ (R : Type u_5) [inst : Zero R] [inst_1 : Pow R ℕ], IsReduced R ↔ ∀ (x : R), IsNilpotent x → x = 0
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Restrict
ContinuousLinearMap.restrict_eq_domRestrict_codRestrict : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4}
  {M₂ : Type u_5} [inst_2 : TopologicalSpace M₁] [inst_3 : AddCommMonoid M₁] [inst_4 : Module R₁ M₁]
  [inst_5 : TopologicalSpace M₂] [inst_6 : AddCommMonoid M₂] [inst_7 : Module R₂ M₂] {f : M₁ →SL[σ₁₂] M₂}
  {p : Submodule R₁ M₁} {q : Submodule R₂ M₂} (hf : ∀ (x : M₁), f x ∈ q),
  f.restrict ⋯ = (f.codRestrict q hf).domRestrict p
-- Init.Data.UInt.Lemmas
UInt32.toUInt64_ofNatClamp_of_lt : ∀ {n : ℕ} (hn : n < UInt32.size), (UInt32.ofNatClamp n).toUInt64 = UInt64.ofNatLT n ⋯
-- Mathlib.Analysis.ODE.PicardLindelof
ODE.FunSpace.mk.sizeOf_spec : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {tmin tmax : ℝ} {t₀ : ↑(Set.Icc tmin tmax)} {x₀ : E} {r L : NNReal}
  [inst_1 : SizeOf E] (toFun : ↑(Set.Icc tmin tmax) → E) (lipschitzWith : LipschitzWith L toFun)
  (mem_closedBall₀ : toFun t₀ ∈ Metric.closedBall x₀ ↑r),
  sizeOf { toFun := toFun, lipschitzWith := lipschitzWith, mem_closedBall₀ := mem_closedBall₀ } =
    1 + sizeOf mem_closedBall₀
-- Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
CategoryTheory.MorphismProperty.Over.map_map_left : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] {P : CategoryTheory.MorphismProperty T}
  (Q : CategoryTheory.MorphismProperty T) [inst_1 : Q.IsMultiplicative] {X Y : T} [inst_2 : P.IsStableUnderComposition]
  {f : X ⟶ Y} (hPf : P f)
  {X_1 Y_1 :
    CategoryTheory.MorphismProperty.Comma (CategoryTheory.Functor.id T) (CategoryTheory.Functor.fromPUnit X) P Q ⊤}
  (f_1 : X_1 ⟶ Y_1),
  ((CategoryTheory.MorphismProperty.Over.map Q hPf).map f_1).left =
    (CategoryTheory.MorphismProperty.Comma.Hom.hom f_1).left
-- Mathlib.CategoryTheory.Sites.PreservesLimits
instPreservesFiniteCoproductsSheafTypeUliftYonedaOfPreservesFiniteProductsOppositeObjFunctorIsSheaf : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  [inst_1 : J.Subcanonical]
  [∀ (X : CategoryTheory.Sheaf J (Type (max v v'))), CategoryTheory.Limits.PreservesFiniteProducts X.obj],
  CategoryTheory.Limits.PreservesFiniteCoproducts (CategoryTheory.GrothendieckTopology.uliftYoneda.{v', v, u} J)
-- Mathlib.Tactic.Positivity.Core
/-- Converts a `MetaM Strictness` which can return `.none`
into one which never returns `.none` but fails instead.  -/
Mathlib.Meta.Positivity.throwNone : {u : Lean.Level} →
  {α : Q(Type u)} →
    {zα : Q(Zero «$α»)} →
      {e : Q(«$α»)} →
        {pα? : Option Q(PartialOrder «$α»)} →
          Lean.MetaM (Mathlib.Meta.Positivity.Strictness zα e pα?) →
            Lean.MetaM (Mathlib.Meta.Positivity.Strictness zα e pα?)
-- Mathlib.Analysis.Normed.Group.Continuity
SeminormedAddGroup.uniformCauchySeqOnFilter_iff_tendstoUniformlyOnFilter_zero : ∀ {ι : Type u_2} {κ : Type u_3} {G : Type u_6} [inst : SeminormedAddGroup G] {f : ι → κ → G} {l : Filter ι}
  {l' : Filter κ},
  UniformCauchySeqOnFilter f l l' ↔ TendstoUniformlyOnFilter (fun n z => -f n.1 z + f n.2 z) 0 (l ×ˢ l) l'
-- Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
/-- For any valuation `v` compatible with the valuative relation on `R`, the closed unit ball
around zero `{x | v x ≤ 1}` is open in the valuative topology.  -/
Valuation.isOpen_integer : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : ValuativeRel R] {Γ₀ : Type u_3} [inst_2 : LinearOrderedCommGroupWithZero Γ₀]
  [_t : TopologicalSpace R] [IsValuativeTopology R] {v : Valuation R Γ₀} [v.Compatible], IsOpen ↑v.integer
-- Mathlib.Computability.PartrecCode
Nat.Partrec.Code.right : Nat.Partrec.Code
-- Lean.Elab.Term.TermElabM
/-- Apply given attributes **at** a given application time  -/
Lean.Elab.Term.applyAttributesAt : Lean.Name → Array Lean.Elab.Attribute → Lean.AttributeApplicationTime → Lean.Elab.TermElabM Unit
-- Batteries.Data.PairingHeap
/-- `O(1)`. Returns the smallest element in the heap, or panics if the heap is empty.  -/
Batteries.PairingHeap.head! : {α : Type u} → {le : α → α → Bool} → [Inhabited α] → Batteries.PairingHeap α le → α
-- Batteries.Lean.Meta.Basic
/-- Check whether a metavariable is assigned or delayed-assigned. A
delayed-assigned metavariable is already 'solved' but the solution cannot be
substituted yet because we have to wait for some other metavariables to be
assigned first. So in most situations you want to treat a delayed-assigned
metavariable as assigned.
 -/
Lean.MetavarContext.isExprMVarAssignedOrDelayedAssigned : Lean.MetavarContext → Lean.MVarId → Bool
-- Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
HomotopicalAlgebra.BifibrantObject.HoCat.ιFibrantObject_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C]
  (X : HomotopicalAlgebra.BifibrantObject C),
  HomotopicalAlgebra.BifibrantObject.HoCat.ιFibrantObject.obj (HomotopicalAlgebra.BifibrantObject.toHoCat.obj X) =
    HomotopicalAlgebra.FibrantObject.toHoCat.obj (HomotopicalAlgebra.BifibrantObject.ιFibrantObject.obj X)
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
/-- The isomorphism between points of limit kernel forks induced by an isomorphism
in the category of arrows.  -/
CategoryTheory.Limits.KernelFork.mapIsoOfIsLimit : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y : C} →
        {f : X ⟶ Y} →
          {X' Y' : C} →
            {f' : X' ⟶ Y'} →
              {kf : CategoryTheory.Limits.KernelFork f} →
                {kf' : CategoryTheory.Limits.KernelFork f'} →
                  CategoryTheory.Limits.IsLimit kf →
                    CategoryTheory.Limits.IsLimit kf' →
                      (CategoryTheory.Arrow.mk f ≅ CategoryTheory.Arrow.mk f') → (kf.pt ≅ kf'.pt)
-- Mathlib.Algebra.Group.Subsemigroup.Operations
AddSubsemigroup.range_subtype : ∀ {M : Type u_1} [inst : Add M] (s : AddSubsemigroup M), (AddMemClass.subtype s).srange = s
-- Mathlib.CategoryTheory.Adjunction.PartialAdjoint
CategoryTheory.Functor.partialRightAdjoint_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) {X Y : F.PartialRightAdjointSource} (f : X ⟶ Y),
  F.partialRightAdjoint.map f = F.partialRightAdjointMap f
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.const.eq_1 : ∀ (α : Type u_1) {β : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace β]
  (b : β), MeasureTheory.AEEqFun.const α b = MeasureTheory.AEEqFun.mk (fun x => b) ⋯
-- Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
CategoryTheory.ObjectProperty.instIsClosedUnderLimitsOfShapeTop : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (J : Type u')
  [inst_1 : CategoryTheory.Category.{v', u'} J], ⊤.IsClosedUnderLimitsOfShape J
-- Mathlib.GroupTheory.Generators
Group.Generators.mk : {G : Type u_5} →
  [inst : Group G] → {ι : Type u_6} → (val : ι → G) → Subgroup.closure (Set.range val) = ⊤ → Group.Generators G ι
-- Mathlib.CategoryTheory.ObjectProperty.Small
CategoryTheory.ObjectProperty.EssentiallySmall.exists_small : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C)
  [P.IsClosedUnderIsomorphisms] [CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} P],
  ∃ P₀, ∃ (_ : CategoryTheory.ObjectProperty.Small.{w, v, u} P₀), P = P₀.isoClosure
-- Mathlib.Analysis.Calculus.FDeriv.Analytic
/-- If a function is analytic on an open set `s`, so is its derivative.  -/
AnalyticOnNhd.deriv_of_isOpen : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {s : Set 𝕜}, AnalyticOnNhd 𝕜 f s → IsOpen s → AnalyticOnNhd 𝕜 (deriv f) s
-- Mathlib.Topology.FiberBundle.Constructions
Bundle.Trivial.fiberBundle_trivializationAtlas' : ∀ (B : Type u_1) (F : Type u_2) [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F],
  FiberBundle.trivializationAtlas' = {Bundle.Trivial.trivialization B F}
-- Mathlib.Data.Finset.Basic
/-- **Alias** of the reverse direction of `Finset.attach_nonempty_iff`. -/
Finset.Nonempty.attach : ∀ {α : Type u_1} {s : Finset α}, s.Nonempty → s.attach.Nonempty
-- Mathlib.Data.EReal.Operations
/-- negation on `EReal`  -/
EReal.neg : EReal → EReal
-- Mathlib.Algebra.Ring.Defs
NonUnitalRing.mk : {α : Type u_1} →
  [toNonUnitalNonAssocRing : NonUnitalNonAssocRing α] → (∀ (a b c : α), a * b * c = a * (b * c)) → NonUnitalRing α
-- Mathlib.Logic.Equiv.Set
Equiv.ofLeftInverse.congr_simp : ∀ {α : Sort u_3} {β : Type u_4} (f : α → β) (f_inv f_inv_1 : Nonempty α → β → α) (e_f_inv : f_inv = f_inv_1)
  (hf : ∀ (h : Nonempty α), Function.LeftInverse (f_inv h) f),
  Equiv.ofLeftInverse f f_inv hf = Equiv.ofLeftInverse f f_inv_1 ⋯
-- Mathlib.NumberTheory.ModularForms.SlashActions
_private.Mathlib.NumberTheory.ModularForms.SlashActions.0.ModularForm.zero_slash : ∀ (k : ℤ) (A : GL (Fin 2) ℝ), ModularForm.privateSlash✝ k A 0 = 0
-- Init.Grind.Ring.CommSemiringAdapter
Lean.Grind.CommRing.Expr.toPolyS.match_4.congr_eq_9 : ∀ (motive : Lean.Grind.CommRing.Expr → Sort u_1) (x : Lean.Grind.CommRing.Expr)
  (h_1 : (n : ℤ) → motive (Lean.Grind.CommRing.Expr.num n))
  (h_2 : (x : Lean.Grind.CommRing.Var) → motive (Lean.Grind.CommRing.Expr.var x))
  (h_3 : (a b : Lean.Grind.CommRing.Expr) → motive (a.add b))
  (h_4 : (a b : Lean.Grind.CommRing.Expr) → motive (a.mul b))
  (h_5 : (a : Lean.Grind.CommRing.Expr) → (k : ℕ) → motive (a.pow k))
  (h_6 : (n : ℕ) → motive (Lean.Grind.CommRing.Expr.natCast n))
  (h_7 : (a b : Lean.Grind.CommRing.Expr) → motive (a.sub b)) (h_8 : (a : Lean.Grind.CommRing.Expr) → motive a.neg)
  (h_9 : (k : ℤ) → motive (Lean.Grind.CommRing.Expr.intCast k)) (k : ℤ),
  x = Lean.Grind.CommRing.Expr.intCast k →
    (match x with
      | Lean.Grind.CommRing.Expr.num n => h_1 n
      | Lean.Grind.CommRing.Expr.var x => h_2 x
      | a.add b => h_3 a b
      | a.mul b => h_4 a b
      | a.pow k => h_5 a k
      | Lean.Grind.CommRing.Expr.natCast n => h_6 n
      | a.sub b => h_7 a b
      | a.neg => h_8 a
      | Lean.Grind.CommRing.Expr.intCast k => h_9 k) ≍
      h_9 k
-- Mathlib.Analysis.Normed.Affine.Simplex
/-- A simplex is scalene if all the edge lengths are different.  -/
Affine.Simplex.Scalene : {R : Type u_1} →
  {V : Type u_2} →
    {P : Type u_3} →
      [inst : Ring R] →
        [inst_1 : SeminormedAddCommGroup V] →
          [inst_2 : PseudoMetricSpace P] →
            [inst_3 : Module R V] → [inst_4 : NormedAddTorsor V P] → {n : ℕ} → Affine.Simplex R P n → Prop
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousAddEquiv.trans_apply : ∀ {M : Type u_1} {N : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace N] [inst_2 : Add M]
  [inst_3 : Add N] {L : Type u_3} [inst_4 : Add L] [inst_5 : TopologicalSpace L] (e₁ : M ≃ₜ+ N) (e₂ : N ≃ₜ+ L) (m : M),
  (e₁.trans e₂) m = e₂ (e₁ m)
-- Init.Data.String.Lemmas.Splits
_private.Init.Data.String.Lemmas.Splits.0.String.Slice.Pos.ofEqAppend.eq_1 : ∀ {s : String.Slice} {t₁ t₂ : String} (h : s.copy = t₁ ++ t₂), String.Slice.Pos.ofEqAppend h = s.pos t₁.rawEndPos ⋯
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.ae_restrict_iff'₀ : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {p : α → Prop},
  MeasureTheory.NullMeasurableSet s μ → ((∀ᵐ (x : α) ∂μ.restrict s, p x) ↔ ∀ᵐ (x : α) ∂μ, x ∈ s → p x)
-- Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
MeasureTheory.lpNorm_sub_le_lpNorm_sub_add_lpNorm_sub : ∀ {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] {f g h : α → E},
  MeasureTheory.MemLp f p μ →
    MeasureTheory.MemLp g p μ →
      1 ≤ p → MeasureTheory.lpNorm (f - h) p μ ≤ MeasureTheory.lpNorm (f - g) p μ + MeasureTheory.lpNorm (g - h) p μ
-- Mathlib.CategoryTheory.Shift.Adjunction
/-- Auxiliary definition for `iso`.  -/
CategoryTheory.Adjunction.LeftAdjointCommShift.iso' : {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] →
        {F : CategoryTheory.Functor C D} →
          {G : CategoryTheory.Functor D C} →
            (F ⊣ G) →
              {A : Type u_3} →
                [inst_2 : AddGroup A] →
                  [inst_3 : CategoryTheory.HasShift C A] →
                    [inst_4 : CategoryTheory.HasShift D A] →
                      (a b : A) →
                        a + b = 0 →
                          [G.CommShift A] →
                            (CategoryTheory.shiftFunctor C a).comp F ≅ F.comp (CategoryTheory.shiftFunctor D a)
-- Plausible.Testable
/-- Give up when a well-formed example cannot be generated.
`gaveUp n` tells us that `n` invalid examples were tried.
 -/
Plausible.TestResult.gaveUp : {p : Prop} → ℕ → Plausible.TestResult p
-- Mathlib.Data.Finite.Defs
Equiv.infinite_iff : ∀ {α : Sort u_1} {β : Sort u_2} (e : α ≃ β), Infinite α ↔ Infinite β
-- Mathlib.Analysis.Normed.Group.Uniform
AntilipschitzWith.le_mul_nnnorm' : ∀ {E : Type u_2} {F : Type u_3} [inst : SeminormedGroup E] [inst_1 : SeminormedGroup F] {f : E → F} {K : NNReal},
  AntilipschitzWith K f → f 1 = 1 → ∀ (x : E), ‖x‖₊ ≤ K * ‖f x‖₊
-- Mathlib.Tactic.TacticAnalysis.Declarations
/-- Whether to report when a tactic can be replaced with itself.

When true (default), all successful replacements are reported, including when
the suggested tactic matches the existing proof.
When false, self-replacements are suppressed.
 -/
linter.tacticAnalysis.tryAtEachStep.selfReplacements : Lean.Option Bool
-- Std.Data.HashSet.Lemmas
Std.HashSet.getD_union : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {k fallback : α},
  (m₁ ∪ m₂).getD k fallback = m₂.getD k (m₁.getD k fallback)
-- Mathlib.Algebra.Order.Monoid.Canonical.Defs
min_add_distrib : ∀ {α : Type u} [inst : AddMonoid α] [inst_1 : LinearOrder α] [CanonicallyOrderedAdd α] (a b c : α),
  min a (b + c) = min a (min a b + min a c)
-- Mathlib.Order.Partition.Basic
Partition.ext_iff : ∀ {α : Type u_1} {s : α} [inst : CompleteLattice α] {P Q : Partition s}, P = Q ↔ ∀ (x : α), x ∈ P ↔ x ∈ Q
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
CategoryTheory.Limits.PushoutCocone.IsColimit.inr_desc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z}
  {t : CategoryTheory.Limits.PushoutCocone f g} (ht : CategoryTheory.Limits.IsColimit t) {W : C} (h : Y ⟶ W) (k : Z ⟶ W)
  (w : CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g k),
  CategoryTheory.CategoryStruct.comp t.inr (CategoryTheory.Limits.PushoutCocone.IsColimit.desc ht h k w) = k
-- Mathlib.NumberTheory.Pell
Pell.Solution₁.y_inv : ∀ {d : ℤ} (a : Pell.Solution₁ d), a⁻¹.y = -a.y
-- Mathlib.Topology.Algebra.InfiniteSum.Ring
/-- The **Cauchy product formula** for the product of two infinite sums indexed by `ℕ`, expressed
by summing on `Finset.HasAntidiagonal.antidiagonal`.

See also `tsum_mul_tsum_eq_tsum_sum_antidiagonal_of_summable_norm` if `f` and `g` are absolutely
summable.  -/
Summable.tsum_mul_tsum_eq_tsum_sum_antidiagonal : ∀ {α : Type u_3} {A : Type u_4} [inst : AddCommMonoid A] [inst_1 : Finset.HasAntidiagonal A]
  [inst_2 : TopologicalSpace α] [inst_3 : NonUnitalNonAssocSemiring α] {f g : A → α} [T3Space α]
  [IsTopologicalSemiring α],
  Summable f →
    Summable g →
      (Summable fun x => f x.1 * g x.2) →
        (∑' (n : A), f n) * ∑' (n : A), g n = ∑' (n : A), ∑ kl ∈ Finset.HasAntidiagonal.antidiagonal n, f kl.1 * g kl.2
-- Mathlib.Data.Nat.Log
Nat.log.go.eq_def : ∀ (n a a_1 : ℕ),
  Nat.log.go n a a_1 =
    match a, a_1 with
    | x, 0 => (n, 0)
    | b, fuel.succ =>
      if n < b then (n, 0)
      else
        match Nat.log.go n (b * b) fuel with
        | (q, e) => if q < b then (q, 2 * e) else (q / b, 2 * e + 1)
-- Init.Data.BitVec.Lemmas
BitVec.shiftLeftZeroExtend.eq_1 : ∀ {w : ℕ} (msbs : BitVec w) (m : ℕ), msbs.shiftLeftZeroExtend m = (msbs.toNat <<< m)#'⋯