mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
/-- Hölder's inequality, as an inequality on the `ℒp` seminorm of an elementwise operation
`fun x => b (f x) (g x)`.  -/
MeasureTheory.eLpNorm_le_eLpNorm_mul_eLpNorm_of_nnnorm : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {m : MeasurableSpace α} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedAddCommGroup G] {μ : MeasureTheory.Measure α} {f : α → E} {g : α → F}
  {p q r : ENNReal},
  MeasureTheory.AEStronglyMeasurable f μ →
    MeasureTheory.AEStronglyMeasurable g μ →
      ∀ (b : E → F → G) (c : NNReal),
        (∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊) →
          ∀ [hpqr : p.HolderTriple q r],
            MeasureTheory.eLpNorm (fun x => b (f x) (g x)) r μ ≤
              ↑c * MeasureTheory.eLpNorm f p μ * MeasureTheory.eLpNorm g q μ
-- Mathlib.Geometry.Euclidean.PerpBisector
AffineSubspace.mem_perpBisector_iff_inner_eq_inner : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {c p₁ p₂ : P},
  c ∈ AffineSubspace.perpBisector p₁ p₂ ↔ inner ℝ (c -ᵥ p₁) (p₂ -ᵥ p₁) = inner ℝ (c -ᵥ p₂) (p₁ -ᵥ p₂)
-- Mathlib.Data.Part
Part.some_sdiff_some : ∀ {α : Type u_1} [inst : SDiff α] (a b : α), Part.some a \ Part.some b = Part.some (a \ b)
-- Init.Data.Sum.Lemmas
Sum.bnot_isRight : ∀ {α : Type u_1} {β : Type u_2} (x : α ⊕ β), (!x.isRight) = x.isLeft
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.get!.congr_simp : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [inst : Std.LawfulEqCmp cmp]
  (t t_1 : Std.DTreeMap.Raw α β cmp), t = t_1 → ∀ (a : α) [inst_1 : Inhabited (β a)], t.get! a = t_1.get! a
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
NumberField.mixedEmbedding.fundamentalCone.hasDerivAt_expMap_single : ∀ {K : Type u_1} [inst : Field K] (w : NumberField.InfinitePlace K) (x : ℝ),
  HasDerivAt (↑(NumberField.mixedEmbedding.fundamentalCone.expMap_single w))
    (NumberField.mixedEmbedding.fundamentalCone.deriv_expMap_single w x) x
-- Std.Data.DHashMap.RawLemmas
/-- Variant of `get_map` that holds with `EquivBEq` (i.e. without `LawfulBEq`).  -/
Std.DHashMap.Raw.Const.get_map' : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {γ : Type w} {m : Std.DHashMap.Raw α fun x => β}
  [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] {f : α → β → γ} {k : α} {h' : k ∈ Std.DHashMap.Raw.map f m}
  (h : m.WF),
  Std.DHashMap.Raw.Const.get (Std.DHashMap.Raw.map f m) k h' = f (m.getKey k ⋯) (Std.DHashMap.Raw.Const.get m k ⋯)
-- Mathlib.Data.List.Iterate
List.getElem?_iterate : ∀ {α : Type u_1} (f : α → α) (a : α) (n i : ℕ), i < n → (List.iterate f a n)[i]? = some (f^[i] a)
-- Mathlib.Data.Finset.Functor
Finset.traverse.eq_1 : ∀ {α β : Type u} {F : Type u → Type u} [inst : Applicative F] [inst_1 : CommApplicative F] [inst_2 : DecidableEq β]
  (f : α → F β) (s : Finset α), Finset.traverse f s = Multiset.toFinset <$> Multiset.traverse f s.val
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
MeasureTheory.FiniteMeasure.instModuleNNReal : {Ω : Type u_3} → [inst : MeasurableSpace Ω] → Module NNReal (MeasureTheory.FiniteMeasure Ω)
-- Lean.Compiler.LCNF.Basic
/-- Return `true` if `decl` is supposed to be inlined/specialized.
 -/
Lean.Compiler.LCNF.Decl.isTemplateLike : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.Decl pu → Lean.CoreM Bool
-- Mathlib.Topology.Order.LocalExtr
IsLocalExtr.comp_continuous : ∀ {α : Type u} {β : Type v} {δ : Type x} [inst : TopologicalSpace α] [inst_1 : Preorder β] {f : α → β}
  [inst_2 : TopologicalSpace δ] {g : δ → α} {b : δ}, IsLocalExtr f (g b) → ContinuousAt g b → IsLocalExtr (f ∘ g) b
-- Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
IncidenceAlgebra.lambda_apply : ∀ (𝕜 : Type u_2) {α : Type u_5} [inst : Zero 𝕜] [inst_1 : One 𝕜] [inst_2 : Preorder α]
  [inst_3 : DecidableRel fun x1 x2 => x1 ⩿ x2] (a b : α), (IncidenceAlgebra.lambda 𝕜) a b = if a ⩿ b then 1 else 0
-- Mathlib.RingTheory.Valuation.RankOne
Valuation.RankOne.toRankLeOne : {R : Type u_1} →
  {Γ₀ : Type u_2} →
    {inst : Ring R} →
      {inst_1 : LinearOrderedCommGroupWithZero Γ₀} → {v : Valuation R Γ₀} → [self : v.RankOne] → v.RankLeOne
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.IsBasis.subset_closure : ∀ {α : Type u_2} {M : Matroid α} {X I : Set α}, M.IsBasis I X → X ⊆ M.closure I
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.lt_add_iff : ∀ {a b c : Ordinal.{u_4}}, c ≠ 0 → (a < b + c ↔ ∃ d < c, a ≤ b + d)
-- Mathlib.Algebra.FreeMonoid.Count
FreeMonoid.count_apply : ∀ {α : Type u_1} [inst : DecidableEq α] (x : α) (l : FreeAddMonoid α),
  (FreeMonoid.count x) l = Multiplicative.ofAdd (List.count x (FreeAddMonoid.toList l))
-- Mathlib.Topology.DiscreteSubset
/-- If `f` is continuous with discrete fibers, then the preimage of discrete sets are discrete.  -/
IsDiscrete.preimage' : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y} {s : Set Y},
  IsDiscrete s → ContinuousOn f (f ⁻¹' s) → (∀ (x : Y), IsDiscrete (f ⁻¹' {x})) → IsDiscrete (f ⁻¹' s)
-- Mathlib.RingTheory.NonUnitalSubring.Defs
/-- A non-unital subring is closed under addition.  -/
NonUnitalSubring.add_mem : ∀ {R : Type u} [inst : NonUnitalNonAssocRing R] (s : NonUnitalSubring R) {x y : R}, x ∈ s → y ∈ s → x + y ∈ s
-- Mathlib.Analysis.Complex.Trigonometric
Complex.cosh_ofReal_im : ∀ (x : ℝ), (Complex.cosh ↑x).im = 0
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey_eq_getKeyD : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {a fallback : α} {h' : a ∈ m}, m.getKey a h' = m.getKeyD a fallback
-- Mathlib.Data.Fin.SuccPredOrder
Fin.orderPred_zero : ∀ (n : ℕ), Order.pred 0 = 0
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.IsClique.mono : ∀ {α : Type u_1} {G H : SimpleGraph α} {s : Set α}, G ≤ H → G.IsClique s → H.IsClique s
-- Mathlib.Algebra.Category.MonCat.Basic
/-- The category of monoids and monoid morphisms.  -/
MonCat : Type (u + 1)
-- Mathlib.Topology.WithTopology
WithTopology.instSemilatticeSup : {X : Type u_1} → (t : TopologicalSpace X) → [SemilatticeSup X] → SemilatticeSup (WithTopology X t)
-- Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
/-- **Alias** of the forward direction of `Matrix.separatingLeft_iff_separatingRight`. -/
Matrix.SeparatingLeft.separatingRight : ∀ {n : Type u_1} {A : Type u_4} [inst : CommRing A] [IsDomain A] {M : Matrix n n A} [inst_2 : Finite n],
  M.SeparatingLeft → M.SeparatingRight
-- Mathlib.Algebra.EuclideanDomain.Defs
/-- A remainder function (denoted `%`) on `R`.
This satisfies the property `b * (a / b) + a % b = a`, where `/` denotes `quotient`.  -/
EuclideanDomain.remainder : {R : Type u} → [self : EuclideanDomain R] → R → R → R
-- Init.Data.UInt.Lemmas
UInt64.lt_irrefl : ∀ (a : UInt64), ¬a < a
-- Init.Data.Array.Lemmas
Array.map_eq_append_iff : ∀ {α : Type u_1} {β : Type u_2} {xs : Array α} {ys zs : Array β} {f : α → β},
  Array.map f xs = ys ++ zs ↔ ∃ as bs, xs = as ++ bs ∧ Array.map f as = ys ∧ Array.map f bs = zs
-- Mathlib.Analysis.FunctionalSpaces.SobolevInequality
MeasureTheory.eLpNormLESNormFDerivOfEqInnerConst.eq_1 : ∀ {E : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E]
  [inst_3 : BorelSpace E] [inst_4 : FiniteDimensional ℝ E] (μ : MeasureTheory.Measure E) [inst_5 : μ.IsAddHaarMeasure]
  (p : ℝ),
  MeasureTheory.eLpNormLESNormFDerivOfEqInnerConst μ p =
    MeasureTheory.eLpNormLESNormFDerivOneConst μ ↑(↑(Module.finrank ℝ E)).conjExponent *
      (p * (↑(Module.finrank ℝ E) - 1) / (↑(Module.finrank ℝ E) - p)).toNNReal
-- Mathlib.Order.Monotone.Defs
instDecidableStrictAntiOnOfForallForallMemSetForallForallForallLt : {α : Type u} →
  {β : Type v} →
    [inst : Preorder α] →
      [inst_1 : Preorder β] →
        {f : α → β} → {s : Set α} → [i : Decidable (∀ a ∈ s, ∀ b ∈ s, a < b → f b < f a)] → Decidable (StrictAntiOn f s)
-- Mathlib.Algebra.Lie.OfAssociative
lie_eq_smul : ∀ {A : Type v} [inst : Ring A] {M : Type w} [inst_1 : AddCommGroup M] [inst_2 : Module A M] (a : A) (m : M),
  ⁅a, m⁆ = a • m
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.memLp_congr_norm : ∀ {α : Type u_1} {E : Type u_4} {F : Type u_5} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F] {f : α → E} {g : α → F},
  MeasureTheory.AEStronglyMeasurable f μ →
    MeasureTheory.AEStronglyMeasurable g μ →
      (∀ᵐ (a : α) ∂μ, ‖f a‖ = ‖g a‖) → (MeasureTheory.MemLp f p μ ↔ MeasureTheory.MemLp g p μ)
-- Mathlib.Order.Filter.Basic
Filter.iSup_inf_principal : ∀ {α : Type u} {ι : Sort x} (f : ι → Filter α) (s : Set α),
  ⨆ i, f i ⊓ Filter.principal s = (⨆ i, f i) ⊓ Filter.principal s
-- Mathlib.CategoryTheory.Yoneda
/-- The identity functor on `Type` is isomorphic to the coyoneda functor coming from `PUnit`.  -/
CategoryTheory.Coyoneda.punitIso : CategoryTheory.coyoneda.obj (Opposite.op PUnit.{v₁ + 1}) ≅ CategoryTheory.Functor.id (Type v₁)
-- Init.Data.List.Lemmas
List.getElem_cons_length : ∀ {α : Type u_1} {x : α} {xs : List α} {i : ℕ} (h : i = xs.length), (x :: xs)[i] = (x :: xs).getLast ⋯
-- Mathlib.CategoryTheory.Shift.Basic
CategoryTheory.Functor.FullyFaithful.hasShift.map_zero_inv_app : ∀ {C : Type u} {A : Type u_1} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_1, u_2} D] [inst_2 : AddMonoid A] [inst_3 : CategoryTheory.HasShift D A]
  {F : CategoryTheory.Functor C D} (hF : F.FullyFaithful) (s : A → CategoryTheory.Functor C C)
  (i : (i : A) → (s i).comp F ≅ F.comp (CategoryTheory.shiftFunctor D i)) (X : C),
  F.map ((CategoryTheory.Functor.FullyFaithful.hasShift.zero hF s i).inv.app X) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorZero D A).inv.app (F.obj X)) ((i 0).inv.app X)
-- Init.Data.String.Basic
String.Pos.Raw.isValid.eq_def : ∀ (s : String) (p : String.Pos.Raw),
  String.Pos.Raw.isValid s p =
    if h : p < s.rawEndPos then decide (s.getUTF8Byte p h).IsUTF8FirstByte else decide (p = s.rawEndPos)
-- Init.Data.UInt.Lemmas
UInt64.lt_trans : ∀ {a b c : UInt64}, a < b → b < c → a < c
-- Mathlib.Data.Fintype.EquivFin
Function.Embedding.toEmbedding_equivOfFiniteSelfEmbedding : ∀ {α : Type u_1} [inst : Finite α] (e : α ↪ α), e.equivOfFiniteSelfEmbedding.toEmbedding = e
-- Mathlib.RepresentationTheory.Coinvariants
Representation.Coinvariants.induction_on : ∀ {k : Type u_1} {G : Type u_2} {V : Type u_3} [inst : CommRing k] [inst_1 : Monoid G] [inst_2 : AddCommGroup V]
  [inst_3 : Module k V] {ρ : Representation k G V} {motive : ρ.Coinvariants → Prop} (x : ρ.Coinvariants),
  (∀ (v : V), motive ((Representation.Coinvariants.mk ρ) v)) → motive x
-- Std.Data.TreeMap.Raw.Basic
/-- Folds the given function over the mappings in the map in ascending order.  -/
Std.TreeMap.Raw.foldl : {α : Type u} →
  {β : Type v} → {cmp : α → α → Ordering} → {δ : Type w} → (δ → α → β → δ) → δ → Std.TreeMap.Raw α β cmp → δ
-- Mathlib.CategoryTheory.Preadditive.Injective.Resolution
/-- the morphism from the single cochain complex with `Z` in degree `0`  -/
CategoryTheory.InjectiveResolution.ι : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroObject C] →
      [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
        {Z : C} → (self : CategoryTheory.InjectiveResolution Z) → (CochainComplex.single₀ C).obj Z ⟶ self.cocomplex
-- Mathlib.SetTheory.Ordinal.Veblen
Ordinal.veblen_right_strictMono : ∀ (o : Ordinal.{u_1}), StrictMono (Ordinal.veblen o)
-- Mathlib.Algebra.Ring.CentroidHom
CentroidHom.coe_neg : ∀ {α : Type u_5} [inst : NonUnitalNonAssocRing α] (f : CentroidHom α), ⇑(-f) = -⇑f
-- Mathlib.Topology.Algebra.FilterBasis
/-- If `R` is discrete then the trivial additive group filter basis on any `R`-module is a
module filter basis.  -/
ModuleFilterBasis.instInhabitedOfDiscreteTopology : {R : Type u_1} →
  {M : Type u_2} →
    [inst : Semiring R] →
      [inst_1 : TopologicalSpace R] →
        [inst_2 : AddCommGroup M] → [inst_3 : Module R M] → [DiscreteTopology R] → Inhabited (ModuleFilterBasis R M)
-- Mathlib.Order.CompleteBooleanAlgebra
/-- **Alias** of `Function.coframeMinimalAxioms`.

---

Pullback an `Order.Coframe.MinimalAxioms` along a function.  -/
Function.Injective.coframeMinimalAxioms : ∀ {α : Type u} {β : Type v} [inst : CompleteLattice α] [inst_1 : CompleteLattice β],
  Order.Coframe.MinimalAxioms β →
    ∀ (f : α → β),
      (∀ {x y : α}, f y ≤ f x ↔ y ≤ x) →
        (∀ (a b : α), f (a ⊔ b) = f a ⊔ f b) →
          (∀ (s : Set α), f (sInf s) = ⨅ a ∈ s, f a) → Order.Coframe.MinimalAxioms α
-- Mathlib.Data.Subtype
Subtype.coe_eq_iff : ∀ {α : Sort u_1} {p : α → Prop} {a : { a // p a }} {b : α}, ↑a = b ↔ ∃ (h : p b), a = ⟨b, h⟩
-- Init.Data.Range.Polymorphic.Iterators
/-- Returns the number of elements contained in the given open range.
 -/
Std.Roo.size : {α : Type u} → [Std.Rxo.HasSize α] → [Std.PRange.UpwardEnumerable α] → Std.Roo α → ℕ
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.δToCycles_cyclesIso_inv_assoc : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.δToCycles_cyclesIso_inv._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.δToCycles_cyclesIso_inv._auto_3) {Z : C}
  (h : (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).cycles ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.δToCycles f₁ f₂ f₃ n₀ n₁ hn₁)
      (CategoryTheory.CategoryStruct.comp (X.cyclesIso f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).inv h) =
    CategoryTheory.CategoryStruct.comp (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).toCycles h
-- Mathlib.Data.Finsupp.Defs
Finsupp.embDomain_zero : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_4} [inst : Zero M] (f : α ↪ β), Finsupp.embDomain f 0 = 0
-- Mathlib.CategoryTheory.CatCommSq
/-- Assuming `[CatCommSq T L R B]`, `iso T L R B` is the isomorphism `T ⋙ R ≅ L ⋙ B`
given by the 2-commutative square.  -/
CategoryTheory.CatCommSq.iso : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {C₃ : Type u_3} →
      {C₄ : Type u_4} →
        {inst : CategoryTheory.Category.{v_1, u_1} C₁} →
          {inst_1 : CategoryTheory.Category.{v_2, u_2} C₂} →
            {inst_2 : CategoryTheory.Category.{v_3, u_3} C₃} →
              {inst_3 : CategoryTheory.Category.{v_4, u_4} C₄} →
                (T : CategoryTheory.Functor C₁ C₂) →
                  (L : CategoryTheory.Functor C₁ C₃) →
                    (R : CategoryTheory.Functor C₂ C₄) →
                      (B : CategoryTheory.Functor C₃ C₄) →
                        [self : CategoryTheory.CatCommSq T L R B] → T.comp R ≅ L.comp B
-- Mathlib.Analysis.Distribution.TemperedDistribution
/-- The partial derivative (or directional derivative) in the direction `m : E` as a
continuous linear map on tempered distributions.  -/
TemperedDistribution.instLineDeriv : {E : Type u_3} →
  {F : Type u_4} →
    [inst : NormedAddCommGroup E] →
      [inst_1 : NormedSpace ℝ E] →
        [inst_2 : AddCommGroup F] →
          [inst_3 : Module ℂ F] →
            [inst_4 : TopologicalSpace F] →
              [IsTopologicalAddGroup F] →
                [ContinuousConstSMul ℂ F] → LineDeriv E (TemperedDistribution E F) (TemperedDistribution E F)
-- Init.Prelude
MonadState.mk : {σ : outParam (Type u)} →
  {m : Type u → Type v} → m σ → (σ → m PUnit.{u + 1}) → ({α : Type u} → (σ → α × σ) → m α) → MonadState σ m
-- Mathlib.CategoryTheory.EffectiveEpi.Comp
CategoryTheory.effectiveEpiFamily_of_effectiveEpi_epi_comp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {α : Type u_2} {B : C} {X Y : α → C}
  (f : (a : α) → X a ⟶ B) (g : (a : α) → Y a ⟶ X a) [∀ (a : α), CategoryTheory.Epi (g a)]
  [CategoryTheory.EffectiveEpiFamily Y fun a => CategoryTheory.CategoryStruct.comp (g a) (f a)],
  CategoryTheory.EffectiveEpiFamily X f
-- Lean.Compiler.LCNF.Basic
_private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.eqImp : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.Code pu → Lean.Compiler.LCNF.Code pu → Bool
-- Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv
_private.Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv.0.GenContFract.squashSeq.match_1.splitter : {K : Type u_1} →
  (motive : Option (GenContFract.Pair K) × Option (GenContFract.Pair K) → Sort u_2) →
    (x : Option (GenContFract.Pair K) × Option (GenContFract.Pair K)) →
      ((gp_n gp_succ_n : GenContFract.Pair K) → motive (some gp_n, some gp_succ_n)) →
        ((x : Option (GenContFract.Pair K) × Option (GenContFract.Pair K)) →
            (∀ (gp_n gp_succ_n : GenContFract.Pair K), x = (some gp_n, some gp_succ_n) → False) → motive x) →
          motive x
-- Init.Data.List.Lemmas
List.reverse_ne_nil_iff : ∀ {α : Type u_1} {xs : List α}, xs.reverse ≠ [] ↔ xs ≠ []
-- Mathlib.GroupTheory.Nilpotent
/-- **Alias** of `Group.nilpotencyClass_zero_iff_subsingleton`. -/
nilpotencyClass_zero_iff_subsingleton : ∀ {G : Type u_1} [inst : Group G] [Group.IsNilpotent G], Group.nilpotencyClass G = 0 ↔ Subsingleton G
-- Mathlib.Combinatorics.Graph.Subgraph
Graph.IsClosedSubgraph.rfl : ∀ {α : Type u_1} {β : Type u_2} {G : Graph α β}, G.IsClosedSubgraph G
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometryEquiv.pointReflection_midpoint_right : ∀ {V : Type u_2} {P : Type u_10} [inst : SeminormedAddCommGroup V] [inst_1 : PseudoMetricSpace P]
  [inst_2 : NormedAddTorsor V P] [inst_3 : NormedSpace ℝ V] (x y : P),
  (AffineIsometryEquiv.pointReflection ℝ (midpoint ℝ x y)) y = x
-- Mathlib.CategoryTheory.Bicategory.Free
/-- `Hom₂.mk η` is an abbreviation for `Quot.mk Rel η`.  -/
CategoryTheory.FreeBicategory.Hom₂.mk : {B : Type u} →
  [inst : Quiver B] →
    {a b : CategoryTheory.FreeBicategory B} → {f g : a ⟶ b} → CategoryTheory.FreeBicategory.Hom₂ f g → (f ⟶ g)
-- Init.Data.Nat.Gcd
Nat.gcd_pos_of_pos_left : ∀ {m : ℕ} (n : ℕ), 0 < m → 0 < m.gcd n
-- Std.Time.DateTime.WallTime
/-- Adds a `Duration` to the given `WallTime`.
 -/
Std.Time.WallTime.addDuration : Std.Time.WallTime → Std.Time.Duration → Std.Time.WallTime
-- Mathlib.GroupTheory.ResiduallyFinite
AddGroup.instResiduallyFiniteOfFinite : ∀ {G : Type u_1} [inst : AddGroup G] [Finite G], AddGroup.ResiduallyFinite G
-- Mathlib.RingTheory.Extension.Generators
Algebra.Generators.ofAlgHom.congr_simp : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {I : Type u_1}
  (f f_1 : MvPolynomial I R →ₐ[R] S) (e_f : f = f_1) (h : Function.Surjective ⇑f),
  Algebra.Generators.ofAlgHom f h = Algebra.Generators.ofAlgHom f_1 ⋯
-- Mathlib.Data.FinEnum.Option
FinEnum.recEmptyOption.eq_def : ∀ {P : Type u → Sort v} (finChoice : (n : ℕ) → Fin (n + 1))
  (congr : {α β : Type u} → (x : FinEnum α) → (x_1 : FinEnum β) → FinEnum.card β = FinEnum.card α → P α → P β)
  (empty : P PEmpty.{u + 1}) (option : {α : Type u} → FinEnum α → P α → P (Option α)) (α : Type u) [inst : FinEnum α],
  FinEnum.recEmptyOption finChoice congr empty option α =
    match cardeq : FinEnum.card α with
    | 0 => congr FinEnum.pempty inst cardeq empty
    | n.succ =>
      let fN := ULift.instFinEnum;
      have this := ⋯;
      congr (FinEnum.insertNone (ULift.{u, 0} (Fin n)) ↑↑(finChoice n)) inst ⋯
        (option fN
          (FinEnum.recEmptyOption finChoice (fun {α β} => congr) empty (fun {α} => option) (ULift.{u, 0} (Fin n))))
-- Mathlib.Topology.Order
TopologicalSpace.indiscrete_iff_forall_inseparable : ∀ {α : Type u} {t : TopologicalSpace α}, IndiscreteTopology α ↔ ∀ (x y : α), Inseparable x y
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
/-- For any `R`-module X, there is a natural `R`-linear map from `X` to `X ⨂ S` by sending `x ↦ x ⊗ 1`
 -/
ModuleCat.ExtendRestrictScalarsAdj.Unit.map : {R : Type u₁} →
  {S : Type u₂} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        (f : R →+* S) → {X : ModuleCat R} → X ⟶ ((ModuleCat.extendScalars f).comp (ModuleCat.restrictScalars f)).obj X
-- Mathlib.Analysis.Distribution.TestFunction
TestFunction.mkCLM.congr_simp : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4} [inst_3 : NormedAddCommGroup F]
  [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace 𝕜 F] {n : ℕ∞} {V : Type u_6} [inst_6 : AddCommGroup V]
  [inst_7 : Module ℝ V] [t : TopologicalSpace V] [inst_8 : IsTopologicalAddGroup V] [inst_9 : ContinuousSMul ℝ V]
  [inst_10 : LocallyConvexSpace ℝ V] [inst_11 : Algebra ℝ 𝕜] [inst_12 : IsScalarTower ℝ 𝕜 F] [inst_13 : Module 𝕜 V]
  [inst_14 : IsScalarTower ℝ 𝕜 V] (toFun toFun_1 : TestFunction Ω F n → V) (e_toFun : toFun = toFun_1)
  (map_add : ∀ (f g : TestFunction Ω F n), toFun (f + g) = toFun f + toFun g)
  (map_smul : ∀ (c : 𝕜) (f : TestFunction Ω F n), toFun (c • f) = c • toFun f)
  (cont :
    ∀ (K : TopologicalSpace.Compacts E) (K_sub_Ω : ↑K ⊆ ↑Ω), Continuous (toFun ∘ TestFunction.ofSupportedIn K_sub_Ω)),
  TestFunction.mkCLM 𝕜 toFun map_add map_smul cont = TestFunction.mkCLM 𝕜 toFun_1 ⋯ ⋯ ⋯
-- Mathlib.CategoryTheory.Functor.ReflectsIso.Jointly
CategoryTheory.JointlyFaithful.jointlyReflectsIsomorphisms : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_4, u_1} C] {I : Type u_2} {D : I → Type u_3}
  [inst_1 : (i : I) → CategoryTheory.Category.{u_5, u_3} (D i)] {F : (i : I) → CategoryTheory.Functor C (D i)}
  [CategoryTheory.Balanced C], CategoryTheory.JointlyFaithful F → CategoryTheory.JointlyReflectIsomorphisms F
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
SheafOfModules.relationsOfIsCokernelFree_I : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : CategoryTheory.HasSheafify J AddCommGrpCat]
  [inst_2 : J.WEqualsLocallyBijective AddCommGrpCat] {ι σ : Type u} {M : SheafOfModules R}
  (f : SheafOfModules.free ι ⟶ SheafOfModules.free σ) (g : SheafOfModules.free σ ⟶ M)
  (H : CategoryTheory.CategoryStruct.comp f g = 0)
  (H' : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ g H)),
  (SheafOfModules.relationsOfIsCokernelFree f g H H').I = ι
-- Mathlib.RingTheory.PowerSeries.Substitution
PowerSeries.HasSubst.smul_X' : ∀ {A : Type u_1} [inst : CommRing A] {R : Type u_2} [inst_1 : CommRing R] [inst_2 : Algebra A R] (a : A),
  PowerSeries.HasSubst (a • PowerSeries.X)
-- Mathlib.Analysis.Convex.Integral
/-- If `μ` is a probability measure on `α`, `s` is a convex closed set in `E`, and `f` is an
integrable function sending `μ`-a.e. points to `s`, then the expected value of `f` belongs to `s`:
`∫ x, f x ∂μ ∈ s`. See also `Convex.sum_mem` for a finite sum version of this lemma.  -/
Convex.integral_mem : ∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [CompleteSpace E] {μ : MeasureTheory.Measure α} {s : Set E} {f : α → E} [MeasureTheory.IsProbabilityMeasure μ],
  Convex ℝ s → IsClosed s → (∀ᵐ (x : α) ∂μ, f x ∈ s) → MeasureTheory.Integrable f μ → ∫ (x : α), f x ∂μ ∈ s
-- Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
UpperHalfPlane.coe_J_smul : ∀ (τ : UpperHalfPlane), ↑(UpperHalfPlane.J • τ) = -(starRingEnd ℂ) ↑τ
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.nonempty_of_mem : ∀ {x u : ZFSet.{u_1}}, x ∈ u → u.Nonempty
-- Lean.Meta.Basic
Lean.Meta.instMonadMetaM : Monad Lean.MetaM
-- Mathlib.Data.Set.Function
Set.injOn_subtype_val : ∀ {α : Type u_1} {p : α → Prop} {s : Set { x // p x }}, Set.InjOn Subtype.val s
-- Mathlib.Algebra.BigOperators.Finprod
/-- For functions with finite support, multiplication commutes with finsums. See `finsum_mul` for a
statement assuming that `R` has no zero divisors.
 -/
finsum_mul' : ∀ {α : Type u_1} {R : Type u_7} [inst : NonUnitalNonAssocSemiring R] (f : α → R) (r : R),
  Function.HasFiniteSupport f → (∑ᶠ (a : α), f a) * r = ∑ᶠ (a : α), f a * r
-- Init.Data.Array.Lemmas
Array.getElem_set_self : ∀ {α : Type u_1} {xs : Array α} {i : ℕ} (h : i < xs.size) {v : α}, (xs.set i v h)[i] = v