mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.DropWhile
_private.Std.Data.Iterators.Lemmas.Combinators.Monadic.DropWhile.0.Std.IterM.step_intermediateDropWhileWithPostcondition.match_3.splitter : {α : Type u_1} →
  {m : Type u_1 → Type u_2} →
    {β : Type u_1} →
      [inst : Std.Iterator α m β] →
        {it : Std.IterM m β} →
          (motive : it.Step → Sort u_3) →
            (x : it.Step) →
              ((it' : Std.IterM m β) →
                  (out : β) →
                    (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩) →
                ((it' : Std.IterM m β) →
                    (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩) →
                  ((h : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩) → motive x
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
ContinuousMultilinearMap.instSMulCommClass : ∀ {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [inst : (i : ι) → AddCommMonoid (M₁ i)] [inst_1 : AddCommMonoid M₂]
  [inst_2 : (i : ι) → TopologicalSpace (M₁ i)] [inst_3 : TopologicalSpace M₂] {R' : Type u_1} {R'' : Type u_2}
  {A : Type u_3} [inst_4 : Semiring A] [inst_5 : (i : ι) → Module A (M₁ i)] [inst_6 : Module A M₂]
  [inst_7 : DistribSMul R' M₂] [inst_8 : ContinuousConstSMul R' M₂] [inst_9 : SMulCommClass A R' M₂]
  [inst_10 : DistribSMul R'' M₂] [inst_11 : ContinuousConstSMul R'' M₂] [inst_12 : SMulCommClass A R'' M₂]
  [SMulCommClass R' R'' M₂], SMulCommClass R' R'' (ContinuousMultilinearMap A M₁ M₂)
-- Mathlib.Data.ENNReal.Basic
ENNReal.le_of_top_imp_top_of_toNNReal_le : ∀ {a b : ENNReal}, (a = ⊤ → b = ⊤) → (a ≠ ⊤ → b ≠ ⊤ → a.toNNReal ≤ b.toNNReal) → a ≤ b
-- Mathlib.GroupTheory.ArchimedeanDensely
/-- Any locally finite linear additive group is archimedean.  -/
Archimedean.of_locallyFiniteOrder : ∀ {G : Type u_2} [inst : AddCommGroup G] [inst_1 : LinearOrder G] [IsOrderedAddMonoid G] [LocallyFiniteOrder G],
  Archimedean G
-- Mathlib.Algebra.Homology.LeftResolution.Basic
CategoryTheory.Abelian.LeftResolution.chainComplexMap_f_1 : ∀ {A : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_1} A] {ι : CategoryTheory.Functor C A}
  (Λ : CategoryTheory.Abelian.LeftResolution ι) {X Y : A} (f : X ⟶ Y) [inst_2 : ι.Full] [inst_3 : ι.Faithful]
  [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_5 : CategoryTheory.Abelian A],
  (Λ.chainComplexMap f).f 1 =
    CategoryTheory.CategoryStruct.comp (Λ.chainComplexXOneIso X).hom
      (CategoryTheory.CategoryStruct.comp
        (Λ.F.map (CategoryTheory.Limits.kernel.map (Λ.π.app X) (Λ.π.app Y) (ι.map (Λ.F.map f)) f ⋯))
        (Λ.chainComplexXOneIso Y).inv)
-- Init.Data.Char.Ordinal
Char.ofOrdinal_injective : Function.Injective Char.ofOrdinal
-- Mathlib.MeasureTheory.Group.MeasurableEquiv
measurableEmbedding_const_smul : ∀ {G : Type u_1} {α : Type u_3} [inst : MeasurableSpace α] [inst_1 : Group G] [inst_2 : MulAction G α]
  [MeasurableConstSMul G α] (c : G), MeasurableEmbedding fun x => c • x
-- Mathlib.Combinatorics.Matroid.Map
Matroid.instRankPosMapEquiv : ∀ {α : Type u_1} {β : Type u_2} {M : Matroid α} [M.RankPos] {f : α ≃ β}, (M.mapEquiv f).RankPos
-- Mathlib.RingTheory.Valuation.RankOne
/-- The inclusion morphism from `Γ₀` to `ℝ≥0`.  -/
Valuation.RankOne.hom : {R : Type u_1} →
  {Γ₀ : Type u_2} →
    [inst : Ring R] →
      [inst_1 : LinearOrderedCommGroupWithZero Γ₀] →
        (v : Valuation R Γ₀) → [hv : v.RankOne] → (MonoidWithZeroHom.ofClass v).ValueGroup₀ →*₀ NNReal
-- Mathlib.RingTheory.Polynomial.ScaleRoots
Polynomial.pow_scaleRoots_of_isReduced : ∀ {R : Type u_1} [inst : CommSemiring R] [IsReduced R] (p : Polynomial R) (r : R) (n : ℕ),
  (p ^ n).scaleRoots r = p.scaleRoots r ^ n
-- Mathlib.LinearAlgebra.TensorPower.Basic
TensorPower.gOne_def : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  GradedMonoid.GOne.one = (PiTensorProduct.tprod R) Fin.elim0
-- Mathlib.Topology.Separation.Regular
RegularSpace.of_exists_mem_nhds_isClosed_subset : ∀ {X : Type u_1} [inst : TopologicalSpace X],
  (∀ (x : X), ∀ s ∈ nhds x, ∃ t ∈ nhds x, IsClosed t ∧ t ⊆ s) → RegularSpace X
-- Mathlib.RingTheory.HahnSeries.Summable
HahnSeries.SummableFamily.instAdd : {Γ : Type u_1} →
  {R : Type u_3} →
    {α : Type u_5} → [inst : PartialOrder Γ] → [inst_1 : AddCommMonoid R] → Add (HahnSeries.SummableFamily Γ R α)
-- Mathlib.Topology.Continuous
/-- See also `IsClosedMap.closure_image_eq_of_continuous`.  -/
image_closure_subset_closure_image : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y} {s : Set X},
  Continuous f → f '' closure s ⊆ closure (f '' s)
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.eval₂_mul_eq_zero_of_left : ∀ {R : Type u} {S : Type v} [inst : Semiring R] {p : Polynomial R} [inst_1 : CommSemiring S] (f : R →+* S) (x : S)
  (q : Polynomial R), Polynomial.eval₂ f x p = 0 → Polynomial.eval₂ f x (p * q) = 0
-- Init.Data.Slice.Array.Iterator
SubarrayIterator.instFinite : ∀ {α : Type u}, Std.Iterators.Finite (SubarrayIterator α) Id
-- Mathlib.Algebra.Order.ToIntervalMod
toIcoMod_sub_self : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b : α), toIcoMod hp a b - b = -toIcoDiv hp a b • p
-- Mathlib.MeasureTheory.Function.ConvergenceInMeasure
MeasureTheory.ExistsSeqTendstoAe.exists_nat_measure_lt_two_inv : ∀ {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : PseudoEMetricSpace E]
  {f : ℕ → α → E} {g : α → E},
  MeasureTheory.TendstoInMeasure μ f Filter.atTop g →
    ∀ (n : ℕ), ∃ N, ∀ m_1 ≥ N, μ {x | 2⁻¹ ^ n ≤ edist (f m_1 x) (g x)} ≤ 2⁻¹ ^ n
-- Init.Data.Range.Polymorphic.UInt
UInt8.rxcHasSize_eq_toBitVec : ∀ {lo : BitVec 8} {hi : UInt8}, Std.Rxc.HasSize.size { toBitVec := lo } hi = Std.Rxc.HasSize.size lo hi.toBitVec
-- Mathlib.SetTheory.Ordinal.Family
/-- Converts a family indexed by an `Ordinal.{u}` to one indexed by a `Type u` using a specified
well-ordering.  -/
Ordinal.familyOfBFamily' : {α : Type u_1} →
  {ι : Type u} →
    (r : ι → ι → Prop) →
      [inst : IsWellOrder ι r] → {o : Ordinal.{u}} → Ordinal.type r = o → ((a : Ordinal.{u}) → a < o → α) → ι → α
-- Mathlib.RingTheory.Ideal.Pointwise
Ideal.IsPrime.smul_iff : ∀ {M : Type u_1} {R : Type u_3} [inst : Group M] [inst_1 : Semiring R] [inst_2 : MulSemiringAction M R] {I : Ideal R}
  (g : M), (g • I).IsPrime ↔ I.IsPrime
-- Mathlib.Analysis.Polynomial.MahlerMeasure
Polynomial.logMahlerMeasure_eq_log_MahlerMeasure : ∀ {p : Polynomial ℂ}, p.logMahlerMeasure = Real.log p.mahlerMeasure
-- Mathlib.Analysis.SpecialFunctions.Complex.Arg
Complex.arg_one : Complex.arg 1 = 0
-- Mathlib.Data.Ordmap.Invariants
Ordnode.findMin'.eq_def : ∀ {α : Type u_1} (x : Ordnode α) (x_1 : α),
  x.findMin' x_1 =
    match x, x_1 with
    | Ordnode.nil, x => x
    | Ordnode.node size l x r, x_2 => l.findMin' x
-- Mathlib.Analysis.Analytic.CPolynomialDef
/-- The sum of a finite power series is continuous.  -/
FormalMultilinearSeries.continuousOn_of_finite : ∀ {𝕜 : 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]
  (p : FormalMultilinearSeries 𝕜 E F) {n : ℕ}, (∀ (m : ℕ), n ≤ m → p m = 0) → Continuous p.sum
-- Mathlib.Topology.DenseEmbedding
/-- If the domain of a `IsDenseEmbedding` is a separable space, then so is its codomain.  -/
IsDenseEmbedding.separableSpace : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {e : α → β}
  [TopologicalSpace.SeparableSpace α], IsDenseEmbedding e → TopologicalSpace.SeparableSpace β
-- Mathlib.Algebra.Lie.Basis.Basic
LieAlgebra.Basis.ext : ∀ {ι : Type u_1} {R : Type u_2} {L : Type u_3} {inst : Finite ι} {inst_1 : CommRing R} {inst_2 : LieRing L}
  {inst_3 : LieAlgebra R L} {H : LieSubalgebra R L} {x y : LieAlgebra.Basis ι H},
  x.A = y.A → x.h = y.h → x.e = y.e → x.f = y.f → x = y
-- Mathlib.Algebra.Group.Embedding
/-- If right-multiplication by any element is cancellative, right-multiplication by `g` is an
embedding.  -/
mulRightEmbedding : {G : Type u_1} → [inst : Mul G] → [IsRightCancelMul G] → G → G ↪ G
-- Mathlib.Order.Interval.Set.Basic
Set.Iic_inj : ∀ {α : Type u_1} [inst : PartialOrder α] {a b : α}, Set.Iic a = Set.Iic b ↔ a = b
-- Lean.Elab.Arg
Lean.Elab.Term.Arg.expr.inj : ∀ {val val_1 : Lean.Expr}, Lean.Elab.Term.Arg.expr val = Lean.Elab.Term.Arg.expr val_1 → val = val_1
-- Mathlib.CategoryTheory.Monad.Limits
CategoryTheory.Comonad.ForgetCreatesLimits'.liftedConeIsLimit_lift_f : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [inst_1 : CategoryTheory.Category.{v, u} J]
  {T : CategoryTheory.Comonad C} {D : CategoryTheory.Functor J T.Coalgebra}
  (c : CategoryTheory.Limits.Cone (D.comp T.forget)) (t : CategoryTheory.Limits.IsLimit c)
  [inst_2 : CategoryTheory.Limits.PreservesLimit (D.comp T.forget) T.toFunctor]
  [inst_3 : CategoryTheory.Limits.PreservesLimit ((D.comp T.forget).comp T.toFunctor) T.toFunctor]
  (s : CategoryTheory.Limits.Cone D),
  ((CategoryTheory.Comonad.ForgetCreatesLimits'.liftedConeIsLimit c t).lift s).f = t.lift (T.forget.mapCone s)
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.Equiv.diff_congr : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp]
  {t₃ t₄ : Std.TreeSet.Raw α cmp}, t₁.WF → t₂.WF → t₃.WF → t₄.WF → t₁.Equiv t₃ → t₂.Equiv t₄ → (t₁ \ t₂).Equiv (t₃ \ t₄)
-- Mathlib.Analysis.Convex.Function
/-- A convex function on a segment is upper-bounded by the max of its endpoints.  -/
ConvexOn.le_on_segment : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommMonoid β] [inst_4 : LinearOrder β] [IsOrderedAddMonoid β] [inst_6 : SMul 𝕜 E] [inst_7 : Module 𝕜 β]
  [PosSMulStrictMono 𝕜 β] {s : Set E} {f : E → β},
  ConvexOn 𝕜 s f → ∀ {x y z : E}, x ∈ s → y ∈ s → z ∈ segment 𝕜 x y → f z ≤ max (f x) (f y)
-- Mathlib.Order.SetNotation
/-- Notation for `Set.sInter` Intersection of a set of sets.  -/
Set.«term⋂₀_» : Lean.ParserDescr
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.find?_toList_eq_some_iff_getKey?_eq_some_and_get?_eq_some : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {k k' : α} {v : β},
      List.find? (fun a => decide (cmp a.1 k = Ordering.eq)) (Std.DTreeMap.Raw.Const.toList t) = some (k', v) ↔
        t.getKey? k = some k' ∧ Std.DTreeMap.Raw.Const.get? t k = some v
-- Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy
HomotopicalAlgebra.FibrantObject.instIsStableUnderPrecompHomRel : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.ModelCategory C],
  CategoryTheory.HomRel.IsStableUnderPrecomp (HomotopicalAlgebra.FibrantObject.homRel C)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getD_filterMap : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β}
  [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] {f : α → β → Option γ} {k : α} {fallback : γ} (h : m.WF),
  (Std.HashMap.Raw.filterMap f m).getD k fallback = (m[k]?.pbind fun x h' => f (m.getKey k ⋯) x).getD fallback
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
WithTop.coe_sSup' : ∀ {α : Type u_1} [inst : LE α] [inst_1 : SupSet α] {s : Set α}, BddAbove s → ↑(sSup s) = sSup ((fun a => ↑a) '' s)
-- Aesop.Forward.State
Aesop.RawHyp.patSubst.inj : ∀ {subst subst_1 : Aesop.Substitution}, Aesop.RawHyp.patSubst subst = Aesop.RawHyp.patSubst subst_1 → subst = subst_1
-- Mathlib.Topology.Algebra.Monoid
ContinuousWithinAt.nsmul : ∀ {M : Type u_3} {X : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace M] [inst_2 : AddMonoid M]
  [ContinuousAdd M] {f : X → M} {x : X} {s : Set X},
  ContinuousWithinAt f s x → ∀ (n : ℕ), ContinuousWithinAt (n • f) s x
-- Mathlib.Algebra.DirectSum.Ring
/-- Multiplication is commutative  -/
DirectSum.GCommRing.mul_comm : ∀ {ι : Type u_1} {A : ι → Type u_2} {inst : AddCommMonoid ι} {inst_1 : (i : ι) → AddCommGroup (A i)}
  [self : DirectSum.GCommRing A] (a b : GradedMonoid A), a * b = b * a
-- Mathlib.RingTheory.MatrixPolynomialAlgebra
matPolyEquiv_symm_C : ∀ {R : Type u_1} [inst : CommSemiring R] {n : Type w} [inst_1 : DecidableEq n] [inst_2 : Fintype n] (M : Matrix n n R),
  matPolyEquiv.symm (Polynomial.C M) = M.map ⇑Polynomial.C
-- Mathlib.Data.Finsupp.Basic
/-- The graph of a finitely supported function over its support, i.e. the finset of input and output
pairs with non-zero outputs.  -/
Finsupp.graph : {α : Type u_1} → {M : Type u_5} → [inst : Zero M] → (α →₀ M) → Finset (α × M)
-- Mathlib.Algebra.Order.Archimedean.Class
FiniteMulArchimedeanClass.lift.congr_simp : ∀ {M : Type u_1} [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M] {α : Type u_2}
  (f f_1 : { a // a ≠ 1 } → α) (e_f : f = f_1)
  (h : ∀ (a b : { a // a ≠ 1 }), FiniteMulArchimedeanClass.mk ↑a ⋯ = FiniteMulArchimedeanClass.mk ↑b ⋯ → f a = f b)
  (a a_1 : FiniteMulArchimedeanClass M),
  a = a_1 → FiniteMulArchimedeanClass.lift f h a = FiniteMulArchimedeanClass.lift f_1 ⋯ a_1
-- Lean.Meta.Sym.Pattern
Lean.Meta.Sym.Pattern.mk.sizeOf_spec : ∀ (levelParams : List Lean.Name) (varTypes : Array Lean.Expr) (varInfos? : Option Lean.Meta.Sym.ProofInstInfo)
  (pattern : Lean.Expr) (fnInfos : Lean.AssocList Lean.Name Lean.Meta.Sym.ProofInstInfo)
  (checkTypeMask? : Option (Array Bool)),
  sizeOf
      { levelParams := levelParams, varTypes := varTypes, varInfos? := varInfos?, pattern := pattern,
        fnInfos := fnInfos, checkTypeMask? := checkTypeMask? } =
    1 + sizeOf levelParams + sizeOf varTypes + sizeOf varInfos? + sizeOf pattern + sizeOf fnInfos +
      sizeOf checkTypeMask?
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.Clopens.mem_mk : ∀ {α : Type u_2} [inst : TopologicalSpace α] {s : Set α} {x : α} {h : IsClopen s},
  x ∈ { carrier := s, isClopen' := h } ↔ x ∈ s
-- Mathlib.CategoryTheory.WithTerminal.Cone
CategoryTheory.WithInitial.coconeEquiv_inverse_obj_ι_app_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type w} [inst_1 : CategoryTheory.Category.{w', w} J]
  {X : C} {K : CategoryTheory.Functor J (CategoryTheory.Under X)}
  (t : CategoryTheory.Limits.Cocone (CategoryTheory.WithInitial.liftFromUnder.obj K)) (a : J),
  ((CategoryTheory.WithInitial.coconeEquiv.inverse.obj t).ι.app a).right = t.ι.app (CategoryTheory.WithInitial.of a)
-- Mathlib.AlgebraicTopology.SimplicialSet.CompStruct
SSet.Edge.CompStruct.ofEq_simplex : ∀ {X : SSet} {x₀ x₁ x₂ y₀ y₁ y₂ : X.obj (Opposite.op { len := 0 })} {e₀₁ : SSet.Edge x₀ x₁} {f₀₁ : SSet.Edge y₀ y₁}
  {e₁₂ : SSet.Edge x₁ x₂} {f₁₂ : SSet.Edge y₁ y₂} {e₀₂ : SSet.Edge x₀ x₂} {f₀₂ : SSet.Edge y₀ y₂}
  (c : e₀₁.CompStruct e₁₂ e₀₂) (h₀₁ : e₀₁.edge = f₀₁.edge) (h₁₂ : e₁₂.edge = f₁₂.edge) (h₀₂ : e₀₂.edge = f₀₂.edge),
  (c.ofEq h₀₁ h₁₂ h₀₂).simplex = c.simplex
-- Mathlib.Algebra.Module.LinearMap.Defs
LinearMap.instSMul : {R : Type u_1} →
  {R₂ : Type u_3} →
    {S : Type u_5} →
      {M : Type u_8} →
        {M₂ : Type u_10} →
          [inst : Semiring R] →
            [inst_1 : Semiring R₂] →
              [inst_2 : AddCommMonoid M] →
                [inst_3 : AddCommMonoid M₂] →
                  [inst_4 : Module R M] →
                    [inst_5 : Module R₂ M₂] →
                      {σ₁₂ : R →+* R₂} → [inst_6 : DistribSMul S M₂] → [SMulCommClass R₂ S M₂] → SMul S (M →ₛₗ[σ₁₂] M₂)
-- Mathlib.Data.ENNReal.Holder
ENNReal.HolderConjugate.inv_add_inv_eq_one : ∀ (p q : ENNReal) [p.HolderConjugate q], p⁻¹ + q⁻¹ = 1
-- Mathlib.MeasureTheory.Group.MeasurableEquiv
MeasurableEquiv.symm_addRight : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : MeasurableSpace G] [inst_2 : MeasurableAdd G] (g : G),
  (MeasurableEquiv.addRight g).symm = MeasurableEquiv.addRight (-g)
-- Mathlib.Algebra.Order.Group.Cyclic
LinearOrderedAddCommGroup.Subgroup.negGen_zmultiples_eq_top : ∀ {G : Type u_1} [inst : AddCommGroup G] [inst_1 : LinearOrder G] [inst_2 : IsOrderedAddMonoid G] (H : AddSubgroup G)
  [inst_3 : Nontrivial ↥H] [hH : IsAddCyclic ↥H],
  AddSubgroup.zmultiples (LinearOrderedAddCommGroup.Subgroup.negGen H) = H
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.image_mul_left' : ∀ {α : Type u_2} [inst : Group α] {t : Set α} {a : α}, (fun x => a⁻¹ * x) '' t = (fun x => a * x) ⁻¹' t
-- Mathlib.Algebra.ContinuedFractions.Computation.Approximations
/-- Shows that `bₙ * Bₙ ≤ Bₙ₊₁`, where `bₙ` is the `n`th partial denominator and `Bₙ₊₁` and `Bₙ` are
the `n + 1`th and `n`th denominator of the continued fraction.  -/
GenContFract.le_of_succ_get?_den : ∀ {K : Type u_1} {v : K} {n : ℕ} [inst : Field K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K]
  [inst_3 : FloorRing K] {b : K},
  (GenContFract.of v).partDens.get? n = some b → b * (GenContFract.of v).dens n ≤ (GenContFract.of v).dens (n + 1)
-- Mathlib.Data.Finset.NAry
Finset.inf'_image₂_left : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} [inst : DecidableEq γ] {f : α → β → γ} {s : Finset α}
  {t : Finset β} [inst_1 : SemilatticeInf δ] (g : γ → δ) (h : (Finset.image₂ f s t).Nonempty),
  (Finset.image₂ f s t).inf' h g = s.inf' ⋯ fun x => t.inf' ⋯ fun x_1 => g (f x x_1)
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Free
PresheafOfModules.free_hom_ext : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  {F : CategoryTheory.Functor Cᵒᵖ (Type u)} {G : PresheafOfModules R} {ψ ψ' : PresheafOfModules.freeObj F ⟶ G},
  CategoryTheory.CategoryStruct.comp (PresheafOfModules.freeAdjunctionUnit R F)
        (CategoryTheory.Functor.whiskerRight ((PresheafOfModules.toPresheaf R).map ψ) (CategoryTheory.forget Ab)) =
      CategoryTheory.CategoryStruct.comp (PresheafOfModules.freeAdjunctionUnit R F)
        (CategoryTheory.Functor.whiskerRight ((PresheafOfModules.toPresheaf R).map ψ') (CategoryTheory.forget Ab)) →
    ψ = ψ'
-- Mathlib.Order.Interval.Finset.Fin
Fin.attachFin_Iic : ∀ {n : ℕ} (a : Fin n), (Finset.Iic ↑a).attachFin ⋯ = Finset.Iic a
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.Const.beqModel.eq_1 : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : BEq β] (l₁ l₂ : List ((_ : α) × β)),
  Std.Internal.List.Const.beqModel l₁ l₂ =
    if l₁.length ≠ l₂.length then false else l₁.all fun x => Std.Internal.List.getValue? x.fst l₂ == some x.snd
-- Aesop.Search.ExpandSafePrefix
Aesop.expandSafePrefix : {Q : Type} → [inst : Aesop.Queue Q] → Aesop.SearchM Q Bool
-- Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete
/-- **Alias** of `CategoryTheory.Functor.toPseudofunctor'`.

---

If `B` is a strict bicategory and `I` is a (1-)category, any functor (of 1-categories) `I ⥤ B` can
be promoted to a pseudofunctor from `LocallyDiscrete I` to `B`.
 -/
CategoryTheory.Functor.toPseudoFunctor' : {I : Type u_1} →
  {B : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} I] →
      [inst_1 : CategoryTheory.Bicategory B] →
        [inst_2 : CategoryTheory.Bicategory.Strict B] →
          CategoryTheory.Functor I B → CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete I) B
-- Mathlib.SetTheory.Cardinal.Defs
Cardinal.mk_plift_false : Cardinal.mk (PLift False) = 0
-- Mathlib.GroupTheory.Solvable
derivedSeries_characteristic : ∀ (G : Type u_1) [inst : Group G] (n : ℕ), (derivedSeries G n).Characteristic
-- Mathlib.Order.Basic
strongLT_of_strongLT_of_le : ∀ {ι : Type u_1} {π : ι → Type u_4} [inst : (i : ι) → Preorder (π i)] {a b c : (i : ι) → π i},
  StrongLT a b → b ≤ c → StrongLT a c
-- Lean.PrettyPrinter.Delaborator.Options
Lean.getPPNotation : Lean.Options → Bool
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.natDegree_monomial : ∀ {R : Type u} [inst : Semiring R] [inst_1 : DecidableEq R] (i : ℕ) (r : R),
  ((Polynomial.monomial i) r).natDegree = if r = 0 then 0 else i
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- Binary biproducts are unique up to isomorphism. This already follows because bilimits are
limits, but in the case of biproducts we can give an isomorphism with particularly nice
definitional properties, namely that `biprod.lift b.fst b.snd` and `biprod.desc b.inl b.inr`
are inverses of each other.  -/
CategoryTheory.Limits.biprod.uniqueUpToIso : {C : Type uC} →
  [inst : CategoryTheory.Category.{uC', uC} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      (X Y : C) →
        [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X Y] →
          {b : CategoryTheory.Limits.BinaryBicone X Y} → b.IsBilimit → (b.pt ≅ X ⊞ Y)
-- Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Associated.card_factors_eq : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α] {a b : α},
  Associated a b → (UniqueFactorizationMonoid.factors a).card = (UniqueFactorizationMonoid.factors b).card
-- Mathlib.Order.Interval.Finset.Fin
Fin.map_castAddEmb_uIcc : ∀ {n : ℕ} (m : ℕ) (i j : Fin n),
  Finset.map (Fin.castAddEmb m) (Finset.uIcc i j) = Finset.uIcc (Fin.castAdd m i) (Fin.castAdd m j)
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
/-- The cocones for `CostructuredArrow.proj L Y ⋙ F`, as a functor from `LeftExtension L F`.  -/
CategoryTheory.Functor.LeftExtension.coconeAtFunctor : {C : Type u_1} →
  {D : Type u_2} →
    {H : Type u_4} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
          [inst_2 : CategoryTheory.Category.{v_4, u_4} H] →
            (L : CategoryTheory.Functor C D) →
              (F : CategoryTheory.Functor C H) →
                (Y : D) →
                  CategoryTheory.Functor (L.LeftExtension F)
                    (CategoryTheory.Limits.Cocone ((CategoryTheory.CostructuredArrow.proj L Y).comp F))
-- Std.Data.TreeMap.Basic
/-- Tries to retrieve the largest key that is less than or equal to the
given key, panicking if no such key exists.
 -/
Std.TreeMap.getKeyLE! : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → [Inhabited α] → Std.TreeMap α β cmp → α → α
-- Aesop.Forward.Substitution
/-- Get the instantiation associated with premise `pi` in `s`. Precondition:
`pi` is in the domain of `s`.  -/
Aesop.Substitution.find? : Aesop.PremiseIndex → Aesop.Substitution → Option Lean.Expr
-- Mathlib.CategoryTheory.Bicategory.Kan.HasKan
CategoryTheory.Bicategory.lanLiftLeftLift_lift : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} (f : b ⟶ a) (g : c ⟶ a)
  [inst_1 : CategoryTheory.Bicategory.HasLeftKanLift f g],
  (CategoryTheory.Bicategory.lanLiftLeftLift f g).lift = CategoryTheory.Bicategory.lanLift f g
-- Mathlib.LinearAlgebra.QuadraticForm.Signature
_private.Mathlib.LinearAlgebra.QuadraticForm.Signature.0.QuadraticForm.sigPos_add_sigNeg_add_radical₁ : ∀ {𝕜 : Type u_4} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] {ι : Type u_5} [inst_2 : Fintype ι] {w : ι → 𝕜}
  [IsStrictOrderedRing 𝕜],
  sigPos (QuadraticMap.weightedSumSquares 𝕜 w) + sigNeg (QuadraticMap.weightedSumSquares 𝕜 w) +
      Module.finrank 𝕜 ↥(QuadraticMap.weightedSumSquares 𝕜 w).radical =
    Nat.card ι
-- Mathlib.SetTheory.Descriptive.Tree
/-- A variant of `List.take` internally to a tree  -/
Descriptive.Tree.take : {A : Type u_1} → {T : ↥(Descriptive.tree A)} → ℕ → ↥T → ↥T
-- Init.GrindInstances.ToInt
Lean.Grind.instDivNatCiOfNatInt : Lean.Grind.ToInt.Div ℕ (Lean.Grind.IntInterval.ci 0)
-- Mathlib.MeasureTheory.Integral.Gamma
integral_exp_neg_mul_rpow : ∀ {p b : ℝ}, 0 < p → 0 < b → ∫ (x : ℝ) in Set.Ioi 0, Real.exp (-b * x ^ p) = b ^ (-1 / p) * Real.Gamma (1 / p + 1)
-- Mathlib.RingTheory.MvPowerSeries.Trunc
MvPowerSeries.ext_trunc' : ∀ {σ : Type u_1} {R : Type u_2} [inst : DecidableEq σ] [inst_1 : CommSemiring R] {f g : MvPowerSeries σ R},
  f = g ↔ ∀ (n : σ →₀ ℕ), (MvPowerSeries.trunc' R n) f = (MvPowerSeries.trunc' R n) g
-- Mathlib.Analysis.Normed.Lp.MeasurableSpace
MeasurableEquiv.toLp_symm_apply : ∀ (p : ENNReal) (X : Type u_1) [inst : MeasurableSpace X] (x : WithLp p X), (MeasurableEquiv.toLp p X).symm x = x.ofLp