mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.SpecialFunctions.CompareExp
/-- If `l : Filter ℂ` is an "exponential comparison filter", then for any complex `a` and any
negative real `b`, we have `(fun z ↦ exp (b * z)) =o[l] (fun z ↦ z ^ a)`.  -/
Complex.IsExpCmpFilter.isLittleO_exp_cpow : ∀ {l : Filter ℂ},
  Complex.IsExpCmpFilter l → ∀ (a : ℂ) {b : ℝ}, b < 0 → (fun z => Complex.exp (↑b * z)) =o[l] fun z => z ^ a
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.Simprocs.pre : Lean.Meta.Simprocs → Lean.Meta.Simp.SimprocTree
-- Init.Data.Nat.Simproc
Nat.Simproc.add_le_add_ge : ∀ (a c : ℕ) {b d : ℕ}, b ≥ d → (a + b ≤ c + d) = (a + (b - d) ≤ c)
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsLimit.nonempty_isLimit_iff_isIso_lift : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {s t : CategoryTheory.Limits.Cone F} (hs : CategoryTheory.Limits.IsLimit s),
  Nonempty (CategoryTheory.Limits.IsLimit t) ↔ CategoryTheory.IsIso (hs.lift t)
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.biprod.inr_snd_assoc : ∀ {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] {Z : C} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr
      (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.snd h) =
    h
-- Mathlib.Algebra.Order.Monoid.Unbundled.Defs
mulRightReflectLT_of_mulLeftReflectLT : ∀ (N : Type u_2) [inst : CommSemigroup N] [inst_1 : LT N] [MulLeftReflectLT N], MulRightReflectLT N
-- Mathlib.Algebra.Homology.HomotopyCategory.Acyclic
/-- The triangulated subcategory of `HomotopyCategory C (ComplexShape.up ℤ)` consisting
of acyclic complexes.  -/
HomotopyCategory.subcategoryAcyclic : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] → CategoryTheory.ObjectProperty (HomotopyCategory C (ComplexShape.up ℤ))
-- Mathlib.Order.Category.PartOrd
/-- Construct a bundled `PartOrd` from the underlying type and typeclass.  -/
PartOrd.of : (carrier : Type u_1) → [str : PartialOrder carrier] → PartOrd
-- Mathlib.CategoryTheory.Sites.SheafHom
/-- The sections of the sheaf `sheafHom F G` identify to morphisms `F ⟶ G`.  -/
CategoryTheory.sheafHomSectionsEquiv : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {A : Type u'} →
        [inst_1 : CategoryTheory.Category.{v', u'} A] →
          (F G : CategoryTheory.Sheaf J A) → ↑(CategoryTheory.sheafHom F G).obj.sections ≃ (F ⟶ G)
-- Mathlib.Order.Filter.AtTopBot.Field
/-- The function `fun x ↦ f x / r` tends to infinity along a nontrivial filter
if and only if `r > 0` and `f` tends to infinity or `r < 0` and `f` tends to negative infinity.  -/
Filter.tendsto_div_const_atTop_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {l : Filter β}
  {f : β → α} {r : α} [l.NeBot],
  Filter.Tendsto (fun x => f x / r) l Filter.atTop ↔
    0 < r ∧ Filter.Tendsto f l Filter.atTop ∨ r < 0 ∧ Filter.Tendsto f l Filter.atBot
-- Mathlib.Algebra.Ring.Pi
/-- Evaluation of functions into an indexed collection of rings at a point is a ring
homomorphism. This is `Function.eval` as a `RingHom`.  -/
Pi.evalRingHom : {I : Type u} → (f : I → Type v) → [inst : (i : I) → NonAssocSemiring (f i)] → (i : I) → ((i : I) → f i) →+* f i
-- Mathlib.Order.BooleanAlgebra.Set
Set.ite_subset_union : ∀ {α : Type u_1} (t s s' : Set α), t.ite s s' ⊆ s ∪ s'
-- Mathlib.Order.Filter.Cofinite
/-- **Alias** of the reverse direction of `Filter.frequently_cofinite_mem_iff_infinite`. -/
Set.Infinite.frequently_cofinite : ∀ {α : Type u_2} {s : Set α}, s.Infinite → ∃ᶠ (x : α) in Filter.cofinite, x ∈ s
-- Mathlib.RingTheory.NonUnitalSubring.Basic
/-- The `NonUnitalSubring` generated by a set includes the set.  -/
NonUnitalSubring.subset_closure : ∀ {R : Type u} [inst : NonUnitalNonAssocRing R] {s : Set R}, s ⊆ ↑(NonUnitalSubring.closure s)
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
CategoryTheory.Functor.OneHypercoverDenseData.mk : {C₀ : Type u₀} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v₀, u₀} C₀] →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        {F : CategoryTheory.Functor C₀ C} →
          {J₀ : CategoryTheory.GrothendieckTopology C₀} →
            {J : CategoryTheory.GrothendieckTopology C} →
              {S : C} →
                (toPreOneHypercoverDenseData : F.PreOneHypercoverDenseData S) →
                  toPreOneHypercoverDenseData.toPreOneHypercover.sieve₀ ∈ J S →
                    (∀ (i₁ i₂ : toPreOneHypercoverDenseData.I₀) ⦃W₀ : C₀⦄ (p₁ : W₀ ⟶ toPreOneHypercoverDenseData.X i₁)
                        (p₂ : W₀ ⟶ toPreOneHypercoverDenseData.X i₂),
                        CategoryTheory.CategoryStruct.comp (F.map p₁) (toPreOneHypercoverDenseData.f i₁) =
                            CategoryTheory.CategoryStruct.comp (F.map p₂) (toPreOneHypercoverDenseData.f i₂) →
                          toPreOneHypercoverDenseData.sieve₁₀ p₁ p₂ ∈ J₀ W₀) →
                      F.OneHypercoverDenseData J₀ J S
-- Mathlib.Order.Partition.Basic
/-- The top partition of `s` is the partition with the single part `s`, or no parts if `s` is the
bottom element.  -/
Partition.instOrderTop : {α : Type u_1} → {s : α} → [inst : CompleteLattice α] → OrderTop (Partition s)
-- Mathlib.Data.Complex.Basic
Complex.normSq_neg : ∀ (z : ℂ), Complex.normSq (-z) = Complex.normSq z
-- Mathlib.Computability.TuringMachine.Tape
Turing.Tape.mk'_left : ∀ {Γ : Type u_1} [inst : Inhabited Γ] (L R : Turing.ListBlank Γ), (Turing.Tape.mk' L R).left = L
-- Init.Data.SInt.Bitwise
Int64.toInt32_and : ∀ (a b : Int64), (a &&& b).toInt32 = a.toInt32 &&& b.toInt32
-- Mathlib.Algebra.Homology.HomotopyCategory
/-- `HomotopyCategory V c` is the category of chain complexes of shape `c` in `V`,
with chain maps identified when they are homotopic.  -/
HomotopyCategory : {ι : Type u_2} →
  (V : Type u) →
    [inst : CategoryTheory.Category.{v, u} V] →
      [CategoryTheory.Preadditive V] → ComplexShape ι → Type (max (max u u_2) v)
-- Init.Data.Array.Lemmas
Array.getElem_singleton : ∀ {α : Type u_1} {a : α} {i : ℕ} (h : i < 1), #[a][i] = a
-- Mathlib.FieldTheory.IsAlgClosed.Spectrum
IsIdempotentElem.quasispectrum_subset : ∀ (𝕜 : Type u_1) {A : Type u_2} [inst : Field 𝕜] [inst_1 : NonUnitalRing A] [inst_2 : Module 𝕜 A] [IsScalarTower 𝕜 A A]
  [SMulCommClass 𝕜 A A] {p : A}, IsIdempotentElem p → quasispectrum 𝕜 p ⊆ {0, 1}
-- Mathlib.Data.Fin.Tuple.Curry
/-- Uncurry all the arguments of `Function.FromTypes p τ` to get
a function from a tuple.

Note this can be used on raw functions if used.  -/
Function.FromTypes.uncurry : {n : ℕ} → {p : Fin n → Type u} → {τ : Type u} → Function.FromTypes p τ → ((i : Fin n) → p i) → τ
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.Measure.neg.eq_1 : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Neg G] (μ : MeasureTheory.Measure G),
  μ.neg = MeasureTheory.Measure.map Neg.neg μ
-- Mathlib.GroupTheory.Coxeter.Length
/-- The homomorphism that sends each element `w : W` to the parity of the length of `w`.
(See `lengthParity_eq_ofAdd_length`.)  -/
CoxeterSystem.lengthParity : {B : Type u_1} →
  {W : Type u_2} → [inst : Group W] → {M : CoxeterMatrix B} → CoxeterSystem M W → W →* Multiplicative (ZMod 2)
-- Lean.Elab.ErrorUtils
_private.Lean.Elab.ErrorUtils.0.Lean.HasOxfordStrings.commaAnd : {α : Sort u_1} → [self : Lean.HasOxfordStrings✝ α] → α
-- Mathlib.CategoryTheory.Pi.Basic
CategoryTheory.NatIso.pi'_hom : ∀ {I : Type w₀} {C : I → Type u₁} [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {E : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} E] {F G : CategoryTheory.Functor E ((i : I) → C i)}
  (e : (i : I) → F.comp (CategoryTheory.Pi.eval C i) ≅ G.comp (CategoryTheory.Pi.eval C i)),
  (CategoryTheory.NatIso.pi' e).hom = CategoryTheory.NatTrans.pi' fun i => (e i).hom
-- Mathlib.CategoryTheory.EssentialImage
CategoryTheory.Functor.EssSurj.toEssImage : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D}, F.toEssImage.EssSurj
-- Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology
/-- **Alias** of `CategoryTheory.Precoverage.toGrothendieck_comap_le_restrictedTopology`. -/
CategoryTheory.Precoverage.toGrothendieck_comap_le_inducedTopology : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} (K : CategoryTheory.Precoverage D),
  (CategoryTheory.Precoverage.comap F K).toGrothendieck ≤ F.restrictedTopology K.toGrothendieck
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.mem_cocycles₁_iff : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A : Rep.{u_1, u, u} k G} (f : G → ↑A),
  f ∈ groupCohomology.cocycles₁ A ↔ ∀ (g h : G), f (g * h) = (A.ρ g) (f h) + f g
-- Lean.Meta.DiscrTree.Types
Lean.Meta.DiscrTree.Key.fvar.inj : ∀ {a : Lean.FVarId} {a_1 : ℕ} {a_2 : Lean.FVarId} {a_3 : ℕ},
  Lean.Meta.DiscrTree.Key.fvar a a_1 = Lean.Meta.DiscrTree.Key.fvar a_2 a_3 → a = a_2 ∧ a_1 = a_3
-- Mathlib.Order.Max
/-- `a : α` is a bottom element of `α` if it is less than or equal to any other element of `α`.
This predicate is roughly an unbundled version of `OrderBot`, except that a preorder may have
several bottom elements. When `α` is linear, this is useful to make a case disjunction on
`NoMinOrder α` within a proof.  -/
IsBot : {α : Type u_1} → [LE α] → α → Prop
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.compQuasiMeasurePreserving.congr_simp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α}
  [inst_1 : TopologicalSpace γ] [inst_2 : MeasurableSpace β] {ν : MeasureTheory.Measure β} (g g_1 : β →ₘ[ν] γ),
  g = g_1 →
    ∀ (f f_1 : α → β) (e_f : f = f_1) (hf : MeasureTheory.Measure.QuasiMeasurePreserving f μ ν),
      g.compQuasiMeasurePreserving f hf = g_1.compQuasiMeasurePreserving f_1 ⋯
-- Mathlib.Probability.ProbabilityMassFunction.Basic
/-- The measure associated to a `PMF` by `toMeasure` is a probability measure.  -/
PMF.toMeasure.isProbabilityMeasure : ∀ {α : Type u_1} [inst : MeasurableSpace α] (p : PMF α), MeasureTheory.IsProbabilityMeasure p.toMeasure
-- Mathlib.Analysis.Normed.Algebra.Exponential
NormedSpace.norm_expSeries_summable : ∀ {𝕂 : Type u_1} {𝔸 : Type u_2} [inst : NontriviallyNormedField 𝕂] [inst_1 : CharZero 𝕂] [ContinuousSMul ℚ 𝕂]
  [inst_3 : NormedRing 𝔸] [inst_4 : NormedAlgebra 𝕂 𝔸] (x : 𝔸),
  Summable fun n => ‖(NormedSpace.expSeries 𝕂 𝔸 n) fun x_1 => x‖
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cone.whiskeringEquivalence_inverse : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (e : K ≌ J),
  (CategoryTheory.Limits.Cone.whiskeringEquivalence e).inverse =
    (CategoryTheory.Limits.Cone.whiskering e.inverse).comp
      (CategoryTheory.Limits.Cone.postcompose (e.invFunIdAssoc F).hom)
-- Mathlib.Analysis.CStarAlgebra.Matrix
Matrix.toEuclideanCLM_toLp : ∀ {𝕜 : Type u_1} {n : Type u_3} [inst : RCLike 𝕜] [inst_1 : Fintype n] [inst_2 : DecidableEq n] (A : Matrix n n 𝕜)
  (x : n → 𝕜), (Matrix.toEuclideanCLM A) (WithLp.toLp 2 x) = WithLp.toLp 2 (A.mulVec x)
-- Init.Data.UInt.Lemmas
UInt64.succ_mul : ∀ {a b : UInt64}, (a + 1) * b = a * b + b
-- Mathlib.Algebra.MonoidAlgebra.Basic
AddMonoidAlgebra.toRingHom_mapAlgHom : ∀ {R : Type u_1} {A : Type u_4} {B : Type u_5} (M : Type u_7) [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Semiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : AddMonoid M] (f : A →ₐ[R] B),
  ↑(AddMonoidAlgebra.mapAlgHom M f) = AddMonoidAlgebra.mapRingHom M f.toRingHom
-- Mathlib.Algebra.Order.Ring.Synonym
OrderDual.instAddCommMonoidWithOne : {R : Type u_1} → [AddCommMonoidWithOne R] → AddCommMonoidWithOne Rᵒᵈ
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
/-- Given `φ : F ⟶ G`, this is the morphism `K ⟶ mappingCone φ` that is constructed
from a cocycle `α : Cochain K F 1` and a cochain `β : Cochain K G 0`
when a suitable cocycle relation is satisfied.  -/
CochainComplex.mappingCone.lift : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {F G : CochainComplex C ℤ} →
        (φ : F ⟶ G) →
          [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] →
            {K : CochainComplex C ℤ} →
              (α : CochainComplex.HomComplex.Cocycle K F 1) →
                (β : CochainComplex.HomComplex.Cochain K G 0) →
                  CochainComplex.HomComplex.δ 0 1 β + (↑α).comp (CochainComplex.HomComplex.Cochain.ofHom φ) ⋯ = 0 →
                    (K ⟶ CochainComplex.mappingCone φ)
-- Mathlib.Combinatorics.Additive.Convolution
/-- Given finite subsets `A` and `B` of a group `G`, convolution of `A` and `B` is a map `G → ℕ`
that maps `x ∈ G` to the number of distinct representations of `x` in the form `x = ab`, where
`a ∈ A`, `b ∈ B`.  -/
Finset.convolution : {G : Type u_1} → [Group G] → [DecidableEq G] → Finset G → Finset G → G → ℕ
-- Mathlib.Order.Interval.Finset.Fin
Fin.map_revPerm_Ioi : ∀ {n : ℕ} (i : Fin n), Finset.map (Equiv.toEmbedding Fin.revPerm) (Finset.Ioi i) = Finset.Iio i.rev
-- Lean.Widget.InteractiveGoal
/-- If true, the goal was not present on the previous tactic state.  -/
Lean.Widget.InteractiveGoal.isInserted? : Lean.Widget.InteractiveGoal → Option Bool
-- Mathlib.Algebra.Divisibility.Units
isRelPrime_one_left : ∀ {α : Type u_1} [inst : CommMonoid α] {x : α}, IsRelPrime 1 x
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.singleOneRingHom.eq_1 : ∀ {k : Type u_1} {G : Type u_2} [inst : Semiring k] [inst_1 : Monoid G] [inst_2 : MulSemiringAction G k],
  SkewMonoidAlgebra.singleOneRingHom =
    { toFun := (↑(SkewMonoidAlgebra.singleAddHom 1)).toFun, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯,
      map_add' := ⋯ }
-- Mathlib.Algebra.Order.AbsoluteValue.Basic
AbsoluteValue.mulHomClass : ∀ {R : Type u_5} {S : Type u_6} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : PartialOrder S],
  MulHomClass (AbsoluteValue R S) R S
-- Mathlib.ModelTheory.Definability
Set.TermDefinable.mono : ∀ {M : Type w} {A : Set M} {L : FirstOrder.Language} [inst : L.Structure M] {α : Type u₁} {B : Set M} {f : (α → M) → M},
  A.TermDefinable L f → A ⊆ B → B.TermDefinable L f
-- Mathlib.Algebra.Group.Action.Defs
SemiconjBy.smul_left_iff : ∀ {G : Type u_3} {H : Type u_4} [inst : Group G] [inst_1 : Mul H] [inst_2 : MulAction G H] [SMulCommClass G H H]
  [IsScalarTower G H H] {a b x : H} {r : G}, SemiconjBy (r • x) a b ↔ SemiconjBy x a b
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.instIsTorsionFreeSubtypeMem : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] (N : LieSubmodule R L M) [Module.IsTorsionFree R M],
  Module.IsTorsionFree R ↥N
-- Mathlib.NumberTheory.ModularForms.Basic
ModularForm.instOneOfNatIntOfHasDetPlusMinusOneFinNatReal : {Γ : Subgroup (GL (Fin 2) ℝ)} → [Γ.HasDetPlusMinusOne] → One (ModularForm Γ 0)
-- Mathlib.Combinatorics.SimpleGraph.Star
SimpleGraph.fromRel.eq_1 : ∀ {V : Type u} (r : V → V → Prop),
  SimpleGraph.fromRel r = { Adj := fun a b => a ≠ b ∧ (r a b ∨ r b a), symm := ⋯, loopless := ⋯ }
-- Mathlib.Topology.Algebra.Group.Basic
Prod.instIsTopologicalAddGroup : ∀ {G : Type w} {H : Type x} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [IsTopologicalAddGroup G]
  [inst_3 : TopologicalSpace H] [inst_4 : AddGroup H] [IsTopologicalAddGroup H], IsTopologicalAddGroup (G × H)
-- Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
MvPolynomial.weightedHomogeneousComponent_finsupp : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] {σ : Type u_3} [inst_1 : AddCommMonoid M] {w : σ → M}
  (φ : MvPolynomial σ R), Function.HasFiniteSupport fun m => (MvPolynomial.weightedHomogeneousComponent w m) φ
-- Aesop.Script.SpecificTactics
_private.Aesop.Script.SpecificTactics.0.Aesop.introsUnfoldingS.tacticBuilder : Lean.Meta.TransparencyMode → Lean.MVarId × Array Lean.FVarId → Aesop.Script.TacticBuilder
-- Mathlib.MeasureTheory.Function.JacobianOneDim
MeasureTheory.integrableOn_Icc_deriv_smul_iff_of_deriv_nonneg : ∀ {F : Type u_1} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] {f f' : ℝ → ℝ} {a b : ℝ} {g : ℝ → F},
  ContinuousOn f (Set.Icc a b) →
    (∀ x ∈ Set.Ioo a b, HasDerivAt f (f' x) x) →
      (∀ x ∈ Set.Ioo a b, 0 ≤ f' x) →
        a ≤ b →
          (MeasureTheory.IntegrableOn (fun x => f' x • g (f x)) (Set.Icc a b) MeasureTheory.volume ↔
            MeasureTheory.IntegrableOn g (Set.Icc (f a) (f b)) MeasureTheory.volume)
-- Mathlib.RingTheory.Localization.Away.Basic
Localization.awayMap_surjective_of_dvd : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_2} [inst_1 : CommSemiring S] (f : R →+* S) {a b : R},
  a ∣ b → Function.Surjective ⇑(Localization.awayMap f a) → Function.Surjective ⇑(Localization.awayMap f b)
-- Mathlib.Data.String.Basic
_private.Mathlib.Data.String.Basic.0.String.Legacy.Iterator.remainingBytes.match_1.splitter : (motive : String.Legacy.Iterator → Sort u_1) →
  (x : String.Legacy.Iterator) → ((s : String) → (i : String.Pos.Raw) → motive { s := s, i := i }) → motive x
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.coyonedaEquiv_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} {F G : CategoryTheory.Functor C (Type v₁)}
  (α : CategoryTheory.coyoneda.obj (Opposite.op X) ⟶ F) (β : F ⟶ G),
  CategoryTheory.coyonedaEquiv (CategoryTheory.CategoryStruct.comp α β) =
    (CategoryTheory.ConcreteCategory.hom (β.app X)) (CategoryTheory.coyonedaEquiv α)
-- Mathlib.Order.BooleanAlgebra.Set
Set.union_sdiff_left : ∀ {α : Type u_1} {s t : Set α}, (s ∪ t) \ s = t \ s
-- Mathlib.Data.NNRat.Floor
NNRat.coe_floor : ∀ (q : ℚ≥0), ↑⌊q⌋₊ = ⌊↑q⌋
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.S_eq : ∀ (R : Type u_1) [inst : CommRing R] (n : ℤ),
  Polynomial.Chebyshev.S R n = Polynomial.X * Polynomial.Chebyshev.S R (n - 1) - Polynomial.Chebyshev.S R (n - 2)
-- Mathlib.Algebra.Order.Monovary
AntivaryOn.div_right₀ : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : LinearOrder α] [inst_1 : Semifield β] [inst_2 : LinearOrder β]
  [IsStrictOrderedRing β] {s : Set ι} {f : ι → α} {g₁ g₂ : ι → β},
  (∀ i ∈ s, 0 ≤ g₁ i) → (∀ i ∈ s, 0 < g₂ i) → AntivaryOn f g₁ s → MonovaryOn f g₂ s → AntivaryOn f (g₁ / g₂) s
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
_private.Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers.0.CategoryTheory.Limits.parallelFamily.match_1.splitter : {J : Type u_1} →
  (motive : (x y : CategoryTheory.Limits.WalkingParallelFamily J) → (x ⟶ y) → Sort u_2) →
    (x y : CategoryTheory.Limits.WalkingParallelFamily J) →
      (h : x ⟶ y) →
        ((x : CategoryTheory.Limits.WalkingParallelFamily J) →
            motive x x (CategoryTheory.Limits.WalkingParallelFamily.Hom.id x)) →
          ((j : J) →
              motive CategoryTheory.Limits.WalkingParallelFamily.zero CategoryTheory.Limits.WalkingParallelFamily.one
                (CategoryTheory.Limits.WalkingParallelFamily.Hom.line j)) →
            motive x y h
-- Mathlib.Analysis.SpecialFunctions.Log.ERealExp
EReal.exp_lt_one_iff : ∀ {a : EReal}, a.exp < 1 ↔ a < 0
-- Mathlib.Algebra.MonoidAlgebra.Degree
AddMonoidAlgebra.Monic.leadingCoeff_mul_eq_right : ∀ {R : Type u_1} {A : Type u_3} {B : Type u_5} [inst : Semiring R] [inst_1 : LinearOrder B] [inst_2 : OrderBot B]
  {p q : AddMonoidAlgebra R A} {D : A → B} [inst_3 : AddZeroClass A] [inst_4 : Add B] [AddLeftStrictMono B]
  [AddRightStrictMono B],
  Function.Injective D →
    (∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2) →
      AddMonoidAlgebra.Monic D p → AddMonoidAlgebra.leadingCoeff D (p * q) = AddMonoidAlgebra.leadingCoeff D q
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.get?_inter_of_contains_eq_false_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α fun x => β}
  [EquivBEq α] [LawfulHashable α],
  (↑m₁).WF → (↑m₂).WF → ∀ {k : α}, m₂.contains k = false → Std.DHashMap.Internal.Raw₀.Const.get? (m₁.inter m₂) k = none
-- Mathlib.LinearAlgebra.Matrix.Transvection
Matrix.TransvectionStruct.toMatrix_reindexEquiv_prod : ∀ {n : Type u_1} {p : Type u_2} {R : Type u₂} [inst : DecidableEq n] [inst_1 : DecidableEq p] [inst_2 : CommRing R]
  [inst_3 : Fintype n] [inst_4 : Fintype p] (e : n ≃ p) (L : List (Matrix.TransvectionStruct n R)),
  (List.map (Matrix.TransvectionStruct.toMatrix ∘ Matrix.TransvectionStruct.reindexEquiv e) L).prod =
    (Matrix.reindexAlgEquiv R R e) (List.map Matrix.TransvectionStruct.toMatrix L).prod
-- Mathlib.Topology.MetricSpace.PiNat
/-- Given a point `x` in a product space `Π (n : ℕ), E n`, and `s` a subset of this space, then
`longestPrefix x s` if the largest `n` for which there is an element of `s` having the same
prefix of length `n` as `x`. If there is no such `n`, use `0` by convention.  -/
PiNat.longestPrefix : {E : ℕ → Type u_2} → ((n : ℕ) → E n) → Set ((n : ℕ) → E n) → ℕ
-- Mathlib.Data.Finset.Lattice.Lemmas
Finset.insert_inter_of_mem : ∀ {α : Type u_1} [inst : DecidableEq α] {s₁ s₂ : Finset α} {a : α}, a ∈ s₂ → insert a s₁ ∩ s₂ = insert a (s₁ ∩ s₂)
-- Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
AddAction.isPreprimitive_of_fixingAddSubgroup_empty_iff : ∀ {G : Type u_1} [inst : AddGroup G] {α : Type u_2} [inst_1 : AddAction G α],
  AddAction.IsPreprimitive ↥(fixingAddSubgroup G ∅) ↥(SubAddAction.ofFixingAddSubgroup G ∅) ↔
    AddAction.IsPreprimitive G α
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.contains_of_contains_erase : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h : t.WF)
  {k a : α},
  Std.DTreeMap.Internal.Impl.contains a (Std.DTreeMap.Internal.Impl.erase k t ⋯).impl = true →
    Std.DTreeMap.Internal.Impl.contains a t = true
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.NeWord.prod.eq_1 : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] {i j : ι} (w : Monoid.CoprodI.NeWord M i j),
  w.prod = w.toWord.prod
-- Lean.Meta.MatchUtil
/-- Matches `e` with `lhs = (rhs : α)` and returns `(α, lhs, rhs)`.  -/
Lean.Meta.matchEq? : Lean.Expr → Lean.MetaM (Option (Lean.Expr × Lean.Expr × Lean.Expr))
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.coe_bot : ∀ {R : Type u} [inst : NonAssocRing R], ↑⊥ = Set.range Int.cast
-- Init.Data.Vector.Lemmas
Vector.back!_mk : ∀ {α : Type u_1} {n : ℕ} [inst : Inhabited α] {xs : Array α} (h : xs.size = n), (Vector.mk xs h).back! = xs.back!
-- Mathlib.Algebra.DirectSum.Basic
_private.Mathlib.Algebra.DirectSum.Basic.0.DFinsupp.extendWith.match_1.eq_2 : ∀ {ι : Type u_1} (motive : Option ι → Sort u_2) (val : ι) (h_1 : Unit → motive none)
  (h_2 : (val : ι) → motive (some val)),
  (match some val with
    | none => h_1 ()
    | some val => h_2 val) =
    h_2 val
-- Mathlib.GroupTheory.Commutator.Basic
AddSubgroup.addCommutator_top_left_le_iff : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G}, ⁅⊤, H⁆ ≤ H ↔ H.Normal
-- Mathlib.Data.Stream.Init
Stream'.get_succ_iterate : ∀ {α : Type u} (n : ℕ) (f : α → α) (a : α), (Stream'.iterate f a).get n.succ = (Stream'.iterate f (f a)).get n
-- Mathlib.Data.Num.Lemmas
Num.ofNat'_one : Num.ofNat' 1 = 1
-- Init.Omega.Constraint
/-- Shorthand for the first component of `tidy`.  -/
Lean.Omega.tidyConstraint : Lean.Omega.Constraint → Lean.Omega.Coeffs → Lean.Omega.Constraint
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.isEmpty_of_isEmpty_insertMany : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} {ρ : Type w}
  [inst : ForIn Id ρ ((a : α) × β a)] [EquivBEq α] [LawfulHashable α] {l : ρ},
  (m.insertMany l).isEmpty = true → m.isEmpty = true
-- Mathlib.RingTheory.PowerSeries.Inverse
/-- Auxiliary function used for computing inverse of a power series  -/
PowerSeries.inv.aux : {R : Type u_1} → [Ring R] → R → PowerSeries R → PowerSeries R