mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
/-- If two sets coincide locally, except maybe at a point, then it is equivalent to have a manifold
derivative within one or the other.  -/
hasMFDerivWithinAt_congr_set' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {x : M} {s t : Set M}
  {f' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)} (y : M),
  s =ᶠ[nhdsWithin x {y}ᶜ] t → (HasMFDerivAt[s] f x f' ↔ HasMFDerivAt[t] f x f')
-- Mathlib.Topology.Algebra.UniformConvergence
UniformOnFun.toFun_pow : ∀ {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} {M : Type u_5} [inst : Pow β M] (c : M) (f : UniformOnFun α β 𝔖),
  (UniformOnFun.toFun 𝔖) (f ^ c) = (UniformOnFun.toFun 𝔖) f ^ c
-- Lean.DocString.Parser
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.arg.potentiallyNamed : ℕ → Lean.Parser.ParserFn
-- Lean.Meta.Tactic.Simp.SimpAll
Lean.Meta.SimpAll.State.diag : Lean.Meta.SimpAll.State → Lean.Meta.Simp.Diagnostics
-- Mathlib.Data.Ordmap.Invariants
Ordnode.Raised.dist_le' : ∀ {n m : ℕ}, Ordnode.Raised n m → m.dist n ≤ 1
-- Lean.Elab.MutualInductive
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.withInductiveLocalDecls.match_1.eq_1 : ∀ (motive : Lean.Expr → Sort u_1) (origFVar : Lean.FVarId)
  (h_1 : (origFVar : Lean.FVarId) → motive (Lean.Expr.fvar origFVar)) (h_2 : (x : Lean.Expr) → motive x),
  (match Lean.Expr.fvar origFVar with
    | Lean.Expr.fvar origFVar => h_1 origFVar
    | x => h_2 x) =
    h_1 origFVar
-- Lean.Data.Lsp.Basic
Lean.Lsp.instFromJsonTextDocumentPositionParams : Lean.FromJson Lean.Lsp.TextDocumentPositionParams
-- Mathlib.Analysis.Distribution.TemperedDistribution
/-- **Alias** of `FourierTransform.fourierCLM_apply`. -/
TemperedDistribution.fourierTransformCLM_apply : ∀ {R : Type u_2} {E : Type u_3} {F : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid E] [inst_2 : AddCommMonoid F]
  [inst_3 : Module R E] [inst_4 : Module R F] [inst_5 : FourierTransform E F] [inst_6 : FourierAdd E F]
  [inst_7 : FourierSMul R E F] [inst_8 : TopologicalSpace E] [inst_9 : TopologicalSpace F]
  [inst_10 : ContinuousFourier E F] (f : E), (FourierTransform.fourierCLM R E) f = FourierTransform.fourier f
-- Mathlib.GroupTheory.Coset.Basic
rightCoset_mem_rightCoset : ∀ {α : Type u_1} [inst : Group α] (s : Subgroup α) {a : α}, a ∈ s → MulOpposite.op a • ↑s = ↑s
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Affine.Simplex.closedInterior_restrict : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] [inst_4 : PartialOrder k] {n : ℕ} (s : Affine.Simplex k P n) {S : AffineSubspace k P}
  (hS : affineSpan k (Set.range s.points) ≤ S), (s.restrict S hS).closedInterior = ⇑S.subtype ⁻¹' s.closedInterior
-- Mathlib.Algebra.Category.Semigrp.Basic
MulEquiv.toSemigrpIso_inv : ∀ {X Y : Type u} [inst : Semigroup X] [inst_1 : Semigroup Y] (e : X ≃* Y),
  e.toSemigrpIso.inv = Semigrp.ofHom e.symm.toMulHom
-- Mathlib.RingTheory.Congruence.Basic
RingCon.instIsScalarTowerQuotient : ∀ {α : Type u_1} {β : Type u_2} {R : Type u_3} [inst : Add R] [inst_1 : MulOneClass R] [inst_2 : SMul α R]
  [inst_3 : IsScalarTower α R R] [inst_4 : SMul β R] [inst_5 : IsScalarTower β R R] (c : RingCon R) [inst_6 : SMul α β]
  [IsScalarTower α β R], IsScalarTower α β c.Quotient
-- Mathlib.SetTheory.Cardinal.Pigeonhole
/-- If an infinite type `β` can be expressed as a union of finite sets,
then the cardinality of the collection of those finite sets
must be at least the cardinality of `β`.  -/
Cardinal.le_range_of_union_finset_eq_univ : ∀ {α : Type u_1} {β : Type u_2} [Infinite β] (f : α → Finset β),
  ⋃ a, ↑(f a) = Set.univ → Cardinal.mk β ≤ Cardinal.mk ↑(Set.range f)
-- Mathlib.Combinatorics.Additive.ETransform
Finset.addDysonETransform_idem : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : AddCommGroup α] (e : α) (x : Finset α × Finset α),
  Finset.addDysonETransform e (Finset.addDysonETransform e x) = Finset.addDysonETransform e x
-- Batteries.Control.AlternativeMonad
OptionT.instLawfulAlternativeOfLawfulMonad : ∀ (m : Type u_1 → Type u_2) [inst : Monad m] [LawfulMonad m], LawfulAlternative (OptionT m)
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.L1.SimpleFunc.setToL1S_add : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  (T : Set α → E →L[ℝ] F),
  (∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0) →
    MeasureTheory.FinMeasAdditive μ T →
      ∀ (f g : ↥(α →₁ₛ[μ] E)),
        MeasureTheory.L1.SimpleFunc.setToL1S T (f + g) =
          MeasureTheory.L1.SimpleFunc.setToL1S T f + MeasureTheory.L1.SimpleFunc.setToL1S T g
-- Mathlib.Algebra.Polynomial.Eval.Coeff
Polynomial.map_surjective : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+* S),
  Function.Surjective ⇑f → Function.Surjective (Polynomial.map f)
-- Init.Data.String.Lemmas.Splits
String.Slice.Pos.Splits.eq_endPos_iff : ∀ {t₁ t₂ : String} {s : String.Slice} {p : s.Pos}, p.Splits t₁ t₂ → (p = s.endPos ↔ t₂ = "")
-- Aesop.Tree.Data
Aesop.GoalState.instToString : ToString Aesop.GoalState
-- Mathlib.Logic.Embedding.Set
Function.Embedding.sigmaSet_preimage : ∀ {α : Type u_1} {ι : Type u_2} {s : ι → Set α} (h : Pairwise (Function.onFun Disjoint s)) (i : ι) (r : Set α),
  Subtype.val '' Sigma.mk i ⁻¹' ⇑(Function.Embedding.sigmaSet h) ⁻¹' r = r ∩ s i
-- Mathlib.Data.Finset.Density
Finset.dens_le_dens_sdiff_add_dens : ∀ {α : Type u_2} [inst : Fintype α] {s t : Finset α} [inst_1 : DecidableEq α], s.dens ≤ (s \ t).dens + t.dens
-- Init.Data.List.Basic
_private.Init.Data.List.Basic.0.List.dropLast.match_1.eq_2 : ∀ {α : Type u_1} (motive : List α → Sort u_2) (head : α) (h_1 : Unit → motive []) (h_2 : (head : α) → motive [head])
  (h_3 : (a : α) → (as : List α) → motive (a :: as)),
  (match [head] with
    | [] => h_1 ()
    | [head] => h_2 head
    | a :: as => h_3 a as) =
    h_2 head
-- Mathlib.CategoryTheory.Whiskering
CategoryTheory.Functor.whiskeringRight_obj_comp : ∀ {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] {D' : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} D'] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D D'),
  ((CategoryTheory.Functor.whiskeringRight E C D).obj F).comp ((CategoryTheory.Functor.whiskeringRight E D D').obj G) =
    (CategoryTheory.Functor.whiskeringRight E C D').obj (F.comp G)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.foldlM_eq_foldlM_toList : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} {δ : Type w} {m : Type w → Type w'}
  [inst : Monad m] [LawfulMonad m] {f : δ → (a : α) → β a → m δ} {init : δ},
  Std.DTreeMap.foldlM f init t = List.foldlM (fun a b => f a b.fst b.snd) init t.toList
-- Mathlib.Topology.Algebra.Group.Basic
isClosedMap_div_right : ∀ {G : Type w} [inst : Group G] [inst_1 : TopologicalSpace G] [IsTopologicalGroup G] (a : G), IsClosedMap fun x => x / a
-- Mathlib.MeasureTheory.Measure.Prod
/-- The Lebesgue integral is measurable. This shows that the integrand of (the right-hand-side of)
the symmetric version of Tonelli's theorem is measurable.  -/
Measurable.lintegral_prod_left' : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  [MeasureTheory.SFinite μ] {f : α × β → ENNReal}, Measurable f → Measurable fun y => ∫⁻ (x : α), f (x, y) ∂μ
-- Lean.Meta.Basic
/-- Low-level version of `MkFreshExprMVar` which allows users to create/reserve a `mvarId` using `mkFreshId`, and then later create
the metavar using this method.  -/
_private.Lean.Meta.Basic.0.Lean.Meta.mkFreshExprMVarWithIdCore : Lean.MVarId →
  Lean.Expr →
    optParam Lean.MetavarKind Lean.MetavarKind.natural →
      optParam Lean.Name Lean.Name.anonymous → optParam ℕ 0 → Lean.MetaM Lean.Expr
-- Mathlib.Analysis.SpecificLimits.Basic
ENNReal.tendsto_pow_atTop_nhds_zero_of_lt_one : ∀ {r : ENNReal}, r < 1 → Filter.Tendsto (fun n => r ^ n) Filter.atTop (nhds 0)
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.GrothendieckTopology.OneHypercover.mem_sieve₁' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {S : C}
  (E : J.OneHypercover S) (i₁ i₂ : E.I₀) [inst_1 : CategoryTheory.Limits.HasPullback (E.f i₁) (E.f i₂)],
  E.sieve₁' i₁ i₂ ∈ J (CategoryTheory.Limits.pullback (E.f i₁) (E.f i₂))
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.Equiv.comm : ∀ {α : Type u} {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β}, m₁.Equiv m₂ ↔ m₂.Equiv m₁
-- Mathlib.Data.Matrix.Diagonal
Matrix.diagonal_intCast' : ∀ {n : Type u_3} {α : Type v} [inst : DecidableEq n] [inst_1 : Zero α] [inst_2 : IntCast α] (m : ℤ),
  Matrix.diagonal ↑m = ↑m
-- Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric
/-- `ordinaryHypergeometricSeries 𝔸 (a b c : 𝕂)` is a `FormalMultilinearSeries`.
Its sum is the `ordinaryHypergeometric` map.  -/
ordinaryHypergeometricSeries : {𝕂 : Type u_1} →
  (𝔸 : Type u_2) →
    [inst : Field 𝕂] →
      [inst_1 : Ring 𝔸] →
        [inst_2 : Algebra 𝕂 𝔸] →
          [inst_3 : TopologicalSpace 𝔸] → [inst_4 : IsTopologicalRing 𝔸] → 𝕂 → 𝕂 → 𝕂 → FormalMultilinearSeries 𝕂 𝔸 𝔸
-- Mathlib.Algebra.GroupWithZero.NonZeroDivisors
mem_nonZeroDivisors_of_ne_zero : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] {x : M₀} [NoZeroDivisors M₀], x ≠ 0 → x ∈ nonZeroDivisors M₀
-- Mathlib.CategoryTheory.Triangulated.Pretriangulated
CategoryTheory.Pretriangulated.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroObject C] →
      [inst_2 : CategoryTheory.HasShift C ℤ] →
        [inst_3 : CategoryTheory.Preadditive C] →
          [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
            (distinguishedTriangles : Set (CategoryTheory.Pretriangulated.Triangle C)) →
              (∀ T₁ ∈ distinguishedTriangles,
                  ∀ (T₂ : CategoryTheory.Pretriangulated.Triangle C) (x : T₂ ≅ T₁), T₂ ∈ distinguishedTriangles) →
                (∀ (X : C), CategoryTheory.Pretriangulated.contractibleTriangle X ∈ distinguishedTriangles) →
                  (∀ {X Y : C} (f : X ⟶ Y),
                      ∃ Z g h, CategoryTheory.Pretriangulated.Triangle.mk f g h ∈ distinguishedTriangles) →
                    (∀ (T : CategoryTheory.Pretriangulated.Triangle C),
                        T ∈ distinguishedTriangles ↔ T.rotate ∈ distinguishedTriangles) →
                      (∀ (T₁ T₂ : CategoryTheory.Pretriangulated.Triangle C),
                          T₁ ∈ distinguishedTriangles →
                            T₂ ∈ distinguishedTriangles →
                              ∀ (a : T₁.obj₁ ⟶ T₂.obj₁) (b : T₁.obj₂ ⟶ T₂.obj₂),
                                CategoryTheory.CategoryStruct.comp T₁.mor₁ b =
                                    CategoryTheory.CategoryStruct.comp a T₂.mor₁ →
                                  ∃ c,
                                    CategoryTheory.CategoryStruct.comp T₁.mor₂ c =
                                        CategoryTheory.CategoryStruct.comp b T₂.mor₂ ∧
                                      CategoryTheory.CategoryStruct.comp T₁.mor₃
                                          ((CategoryTheory.shiftFunctor C 1).map a) =
                                        CategoryTheory.CategoryStruct.comp c T₂.mor₃) →
                        CategoryTheory.Pretriangulated C
-- Mathlib.Algebra.Group.Equiv.Finite
Fintype.decidableEqMulEquivFintype : {α : Type u_4} →
  {β : Type u_5} → [DecidableEq β] → [Fintype α] → [inst : Mul α] → [inst_1 : Mul β] → DecidableEq (α ≃* β)
-- Mathlib.MeasureTheory.Function.L2Space
MeasureTheory.L2.real_inner_indicatorConstLp_one_indicatorConstLp_one : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α} (hs : MeasurableSet s)
  (ht : MeasurableSet t)
  (hμs : autoParam (μ s ≠ ⊤) MeasureTheory.L2.real_inner_indicatorConstLp_one_indicatorConstLp_one._auto_1)
  (hμt : autoParam (μ t ≠ ⊤) MeasureTheory.L2.real_inner_indicatorConstLp_one_indicatorConstLp_one._auto_3),
  inner ℝ (MeasureTheory.indicatorConstLp 2 hs hμs 1) (MeasureTheory.indicatorConstLp 2 ht hμt 1) = μ.real (s ∩ t)
-- Mathlib.Data.Finset.Image
Finset.mem_image_const_self : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] {s : Finset α} {b : β},
  b ∈ Finset.image (Function.const α b) s ↔ s.Nonempty
-- Mathlib.Topology.Instances.NNReal.Lemmas
Real.map_toNNReal_atTop : Filter.map Real.toNNReal Filter.atTop = Filter.atTop
-- Mathlib.CategoryTheory.Limits.ConcreteCategory.Basic
CategoryTheory.Limits.Concrete.isLimit_ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type r}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC] {J : Type w}
  [inst_3 : CategoryTheory.Category.{t, w} J] (F : CategoryTheory.Functor J C)
  [CategoryTheory.Limits.PreservesLimit F (CategoryTheory.forget C)] {D : CategoryTheory.Limits.Cone F}
  (hD : CategoryTheory.Limits.IsLimit D) (x y : CategoryTheory.ToType D.pt),
  (∀ (j : J),
      (CategoryTheory.ConcreteCategory.hom (D.π.app j)) x = (CategoryTheory.ConcreteCategory.hom (D.π.app j)) y) →
    x = y
-- Mathlib.NumberTheory.Divisors
Nat.snd_mem_divisors_of_mem_antidiagonal : ∀ {n : ℕ} {x : ℕ × ℕ}, x ∈ n.divisorsAntidiagonal → x.2 ∈ n.divisors
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.preLeft_map_right : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] {C : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} C] (F : CategoryTheory.Functor C A) (L : CategoryTheory.Functor A T)
  (R : CategoryTheory.Functor B T) {X Y : CategoryTheory.Comma (F.comp L) R} (f : X ⟶ Y),
  ((CategoryTheory.Comma.preLeft F L R).map f).right = f.right
-- Mathlib.NumberTheory.Divisors
Nat.ne_zero_of_mem_divisorsAntidiagonal : ∀ {n : ℕ} {p : ℕ × ℕ}, p ∈ n.divisorsAntidiagonal → p.1 ≠ 0 ∧ p.2 ≠ 0
-- Mathlib.GroupTheory.Submonoid.Inverses
/-- **Alias** of `IsUnit.submonoid.coe_inv`. -/
Submonoid.IsUnit.Submonoid.coe_inv : ∀ {M : Type u_1} [inst : Monoid M] (x : ↥(IsUnit.submonoid M)), ↑x⁻¹ = ↑(IsUnit.unit ⋯)⁻¹
-- Init.Data.String.Lemmas.Search
String.back_toSlice : ∀ {s : String}, s.toSlice.back = s.back
-- Mathlib.Analysis.MeanInequalities
/-- **Alias** of `Real.geom_mean_eq_arith_mean_weighted_iff_of_pos'`.

---

**AM-GM inequality - equality condition**: This theorem provides the equality condition for the
*positive* weighted version of the AM-GM inequality for real-valued nonnegative functions.

The condition is that all elements of `z` are equal to their center of mass `∑ i ∈ s, w i * z i`;
see `geom_mean_eq_arith_mean_weighted_iff_of_pos` for a version that compares the elements to each
other instead.  -/
Real.geom_mean_eq_arith_mean_weighted_iff' : ∀ {ι : Type u} (s : Finset ι) (w z : ι → ℝ),
  (∀ i ∈ s, 0 < w i) →
    ∑ i ∈ s, w i = 1 →
      (∀ i ∈ s, 0 ≤ z i) → (∏ i ∈ s, z i ^ w i = ∑ i ∈ s, w i * z i ↔ ∀ j ∈ s, z j = ∑ i ∈ s, w i * z i)
-- Mathlib.RingTheory.Congruence.Hom
/-- Given ring congruence relations `c, d` on a ring such that `d` contains `c`,
the definition of the homomorphism from the quotient by `c` to the quotient by
`d` induced by `d`'s quotient map.  -/
RingCon.factorₐ_apply : ∀ {M : Type u_1} {R : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring M] [inst_2 : Algebra R M] {c d : RingCon M}
  (h : c ≤ d) (x : c.Quotient), (RingCon.factorₐ R h) x = (c.liftₐ (RingCon.mkₐ R d) ⋯) x
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
CategoryTheory.Limits.FormalCoproduct.evalCompInclIsoId_inv_app_app : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (A : Type u₁) [inst_1 : CategoryTheory.Category.{v₁, u₁} A]
  [inst_2 : CategoryTheory.Limits.HasCoproducts A] (X : CategoryTheory.Functor C A) (X_1 : C),
  ((CategoryTheory.Limits.FormalCoproduct.evalCompInclIsoId C A).inv.app X).app X_1 =
    CategoryTheory.Limits.Sigma.ι (fun x => X.obj X_1) PUnit.unit
-- Mathlib.Data.Nat.Factorial.BigOperators
Nat.prod_factorial_dvd_factorial_sum : ∀ {α : Type u_1} (s : Finset α) (f : α → ℕ), ∏ i ∈ s, (f i).factorial ∣ (∑ i ∈ s, f i).factorial
-- Mathlib.Geometry.Manifold.ContMDiff.Basic
/-- The iterates of `C^n` functions are `C^n`.  -/
ContMDiff.iterate : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {n : WithTop ℕ∞} {f : M → M},
  ContMDiff I I n f → ∀ (k : ℕ), ContMDiff I I n f^[k]
-- Mathlib.CategoryTheory.Limits.Bicones
CategoryTheory.BiconeHom.left : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    (j : J) → CategoryTheory.BiconeHom J CategoryTheory.Bicone.left (CategoryTheory.Bicone.diagram j)
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
Real.log_nonpos : ∀ {x : ℝ}, 0 ≤ x → x ≤ 1 → Real.log x ≤ 0
-- Mathlib.Topology.Order.LowerUpperTopology
/-- The upper topology is the topology generated by the complements of the right-closed left-infinite
intervals.
 -/
Topology.IsUpper : (α : Type u_3) → [t : TopologicalSpace α] → [Preorder α] → Prop
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.pointwise_smul_subset_iff : ∀ {K : Type u} [inst : Field K] {G : Type u_1} [inst_1 : Group G] [inst_2 : MulSemiringAction G K] {g : G}
  {S T : ValuationSubring K}, g • S ≤ T ↔ S ≤ g⁻¹ • T
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Real.abs_cos_sub_cos_le : ∀ (x y : ℝ), |Real.cos x - Real.cos y| ≤ |x - y|
-- Mathlib.Probability.Kernel.Basic
ProbabilityTheory.Kernel.copy.eq_1 : ∀ (α : Type u_4) [inst : MeasurableSpace α],
  ProbabilityTheory.Kernel.copy α = ProbabilityTheory.Kernel.deterministic Function.diag ⋯
-- Mathlib.LinearAlgebra.RootSystem.Reduced
RootPairing.pairing_smul_root_eq_of_not_linearIndependent : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) {i j : ι} [NeZero 2]
  [IsDomain R] [Module.IsTorsionFree R M],
  ¬LinearIndependent R ![P.root i, P.root j] → P.pairing j i • P.root i = 2 • P.root j
-- Lean.Meta.Instances
Lean.Meta.instanceExtension : Lean.SimpleScopedEnvExtension Lean.Meta.InstanceEntry Lean.Meta.Instances
-- Mathlib.CategoryTheory.Enriched.Basic
CategoryTheory.ForgetEnrichment.of_to : ∀ {C : Type u₁} (W : Type v) [inst : CategoryTheory.Category.{w, v} W] [inst_1 : CategoryTheory.MonoidalCategory W]
  [inst_2 : CategoryTheory.EnrichedCategory W C] (X : CategoryTheory.ForgetEnrichment W C),
  CategoryTheory.ForgetEnrichment.of W (CategoryTheory.ForgetEnrichment.to W X) = X
-- Mathlib.Algebra.Group.ModEq
AddCommGroup.modEq_sub : ∀ {G : Type u_1} [inst : AddCommGroup G] (a b : G), a ≡ b [PMOD b - a]
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
/-- The constant cosimplicial object.  -/
CategoryTheory.CosimplicialObject.const : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.Functor C (CategoryTheory.CosimplicialObject C)
-- Mathlib.Order.Category.NonemptyFinLinOrd
/-- Construct a bundled `NonemptyFinLinOrd` from the underlying type and typeclass.  -/
NonemptyFinLinOrd.of : (α : Type u_1) → [Nonempty α] → [Fintype α] → [LinearOrder α] → NonemptyFinLinOrd
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic
/-- The `n`-th Chebyshev polynomial of the first kind evaluates on `cos θ` to the
value `cos (n * θ)`.  -/
Polynomial.Chebyshev.T_real_cos : ∀ (θ : ℝ) (n : ℤ), Polynomial.eval (Real.cos θ) (Polynomial.Chebyshev.T ℝ n) = Real.cos (↑n * θ)
-- Mathlib.CategoryTheory.Category.TwoP
pointedToTwoPFst_map_hom_toFun : ∀ {X Y : Pointed} (f : X ⟶ Y) (a : Option X.X), (pointedToTwoPFst.map f).hom.toFun a = Option.map f.toFun a
-- Mathlib.Topology.IsClosedRestrict
/-- The image by `preimageImageRestrict α S s` of `s` seen as a set of
`Sᶜ.domRestrict ⁻¹' Sᶜ.domRestrict '' s` is a set of
`Sᶜ.domRestrict '' s × (Π i : S, α i)`, and the image of that set by `Prod.snd` is
`S.domRestrict '' s`.

Used in `IsCompact.isClosed_image_restrict` to prove that the restriction of a compact closed set
in a product space to a set of coordinates is closed.  -/
Topology.image_snd_preimageImageRestrict : ∀ {ι : Type u_1} {α : ι → Type u_2} {s : Set ((i : ι) → α i)} {S : Set ι} [inst : (i : ι) → TopologicalSpace (α i)],
  Prod.snd '' ⇑(Homeomorph.preimageImageRestrict α S s) '' (fun x => ↑x) ⁻¹' s = S.domRestrict '' s
-- Mathlib.Topology.Algebra.Module.Basic
Submodule.continuousSMul_quotient : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : TopologicalSpace M] (S : Submodule R M) [inst_4 : TopologicalSpace R] [IsTopologicalAddGroup M]
  [ContinuousSMul R M], ContinuousSMul R (M ⧸ S)
-- Init.Data.Nat.Power2.Basic
_private.Init.Data.Nat.Power2.Basic.0.Nat.isPowerOfTwo_nextPowerOfTwo.isPowerOfTwo_go : ∀ (n power : ℕ) (h₁ : power > 0), power.isPowerOfTwo → (Nat.nextPowerOfTwo.go✝ n power h₁).isPowerOfTwo
-- Init.Data.List.Lemmas
List.ne_nil_of_length_pos : ∀ {α : Type u_1} {l : List α}, 0 < l.length → l ≠ []
-- Mathlib.RingTheory.Radical.Basic
UniqueFactorizationMonoid.exists_dvd_pow_iff_radical_dvd : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] [inst_1 : NormalizationMonoid M] [inst_2 : UniqueFactorizationMonoid M]
  {a b : M}, a ≠ 0 → ((∃ n, a ∣ b ^ n) ↔ UniqueFactorizationMonoid.radical a ∣ b)
-- Mathlib.Data.PNat.Basic
PNat.div_add_mod' : ∀ (m k : ℕ+), m.div k * ↑k + ↑(m.mod k) = ↑m
-- Mathlib.Algebra.Free
/-- The unique magma homomorphism `FreeMagma α →ₙ* FreeMagma β` that sends
each `of x` to `of (f x)`.  -/
FreeMagma.map : {α : Type u} → {β : Type v} → (α → β) → FreeMagma α →ₙ* FreeMagma β
-- Mathlib.CategoryTheory.Equivalence.Symmetry
CategoryTheory.Equivalence.symmEquivInverse_map_app : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] (D : Type u_2)
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {X Y : (D ≌ C)ᵒᵖ} (f : X ⟶ Y) (X_1 : C),
  ((CategoryTheory.Equivalence.symmEquivInverse C D).map f).app X_1 =
    CategoryTheory.CategoryStruct.comp ((Opposite.unop X).inverse.map ((Opposite.unop Y).counitInv.app X_1))
      (CategoryTheory.CategoryStruct.comp
        ((Opposite.unop X).inverse.map
          ((CategoryTheory.Equivalence.asNatTrans f.unop).app ((Opposite.unop Y).inverse.obj X_1)))
        ((Opposite.unop X).unitInv.app ((Opposite.unop Y).inverse.obj X_1)))
-- Mathlib.Data.Fintype.Order
/-- A finite bounded linear order is complete.

If the `α` is already a `BiheytingAlgebra`, then prefer to construct this instance manually using
`Fintype.toCompleteLattice` instead, to avoid creating a diamond with
`LinearOrder.toBiheytingAlgebra`.  -/
Fintype.toCompleteLinearOrder : (α : Type u_2) → [Fintype α] → [inst : LinearOrder α] → [BoundedOrder α] → CompleteLinearOrder α
-- Init.Data.String.Basic
String.instLE : LE String
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
CategoryTheory.Limits.FormalCoproduct.coproductIsoSelf_inv_φ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Limits.FormalCoproduct C) (x : X.I),
  X.coproductIsoSelf.inv.φ x =
    CategoryTheory.CategoryStruct.comp (X.cofanPtIsoSelf.inv.φ x)
      ((CategoryTheory.Limits.FormalCoproduct.coproductIsoCofanPt X.I X.toFun).inv.φ (X.cofanPtIsoSelf.inv.f x))