mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
MeasurableSpace.mk.inj : ∀ {α : Type u_7} {MeasurableSet' : Set α → Prop} {measurableSet_empty : MeasurableSet' ∅}
  {measurableSet_compl : ∀ (s : Set α), MeasurableSet' s → MeasurableSet' sᶜ}
  {measurableSet_iUnion : ∀ (f : ℕ → Set α), (∀ (i : ℕ), MeasurableSet' (f i)) → MeasurableSet' (⋃ i, f i)}
  {MeasurableSet'_1 : Set α → Prop} {measurableSet_empty_1 : MeasurableSet'_1 ∅}
  {measurableSet_compl_1 : ∀ (s : Set α), MeasurableSet'_1 s → MeasurableSet'_1 sᶜ}
  {measurableSet_iUnion_1 : ∀ (f : ℕ → Set α), (∀ (i : ℕ), MeasurableSet'_1 (f i)) → MeasurableSet'_1 (⋃ i, f i)},
  { MeasurableSet' := MeasurableSet', measurableSet_empty := measurableSet_empty,
        measurableSet_compl := measurableSet_compl, measurableSet_iUnion := measurableSet_iUnion } =
      { MeasurableSet' := MeasurableSet'_1, measurableSet_empty := measurableSet_empty_1,
        measurableSet_compl := measurableSet_compl_1, measurableSet_iUnion := measurableSet_iUnion_1 } →
    MeasurableSet' = MeasurableSet'_1
-- Mathlib.Data.Sum.Basic
Sum.LiftRel.exists_of_isLeft_left : ∀ {α : Type u} {β : Type v} {γ : Type u_1} {δ : Type u_2} {r : α → γ → Prop} {s : β → δ → Prop} {x : α ⊕ β} {y : γ ⊕ δ},
  Sum.LiftRel r s x y → x.isLeft = true → ∃ a c, r a c ∧ x = Sum.inl a ∧ y = Sum.inl c
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.center_le_centralizer : ∀ (R : Type u) {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (s : Set A),
  Subalgebra.center R A ≤ Subalgebra.centralizer R s
-- Mathlib.CategoryTheory.Galois.Action
CategoryTheory.PreGaloisCategory.instPreservesFiniteProductsActionFintypeCatAutFunctorFunctorToAction : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (F : CategoryTheory.Functor C FintypeCat)
  [inst_1 : CategoryTheory.GaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F],
  CategoryTheory.Limits.PreservesFiniteProducts (CategoryTheory.PreGaloisCategory.functorToAction F)
-- Mathlib.Algebra.Homology.TotalComplex
HomologicalComplex₂.total.map_comp_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {I₁ : Type u_2}
  {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} {K L M : HomologicalComplex₂ C c₁ c₂}
  (φ : K ⟶ L) (ψ : L ⟶ M) (c₁₂ : ComplexShape I₁₂) [inst_2 : TotalComplexShape c₁ c₂ c₁₂] [inst_3 : DecidableEq I₁₂]
  [inst_4 : K.HasTotal c₁₂] [inst_5 : L.HasTotal c₁₂] [inst_6 : M.HasTotal c₁₂] {Z : HomologicalComplex C c₁₂}
  (h : M.total c₁₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex₂.total.map (CategoryTheory.CategoryStruct.comp φ ψ) c₁₂) h =
    CategoryTheory.CategoryStruct.comp (HomologicalComplex₂.total.map φ c₁₂)
      (CategoryTheory.CategoryStruct.comp (HomologicalComplex₂.total.map ψ c₁₂) h)
-- Init.Data.SInt.Lemmas
Int32.mod_zero : ∀ {a : Int32}, a % 0 = a
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Limits.Cone.overPost_pt : ∀ {J : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] {D : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone D)
  (j : J), (c.overPost j).pt = CategoryTheory.Over.mk (c.π.app j)
-- Mathlib.Algebra.CubicDiscriminant
Cubic.of_a_eq_zero' : ∀ {R : Type u_1} {b c d : R} [inst : Semiring R],
  { a := 0, b := b, c := c, d := d }.toPoly =
    Polynomial.C b * Polynomial.X ^ 2 + Polynomial.C c * Polynomial.X + Polynomial.C d
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
MonoidAlgebra.mapDomainNonUnitalRingHom_apply : ∀ (R : Type u_3) {M : Type u_6} {N : Type u_7} [inst : Semiring R] [inst_1 : Mul M] [inst_2 : Mul N] (f : M →ₙ* N)
  (x : MonoidAlgebra R M), (MonoidAlgebra.mapDomainNonUnitalRingHom R f) x = MonoidAlgebra.mapDomain (⇑f) x
-- Mathlib.CategoryTheory.Abelian.Indization
CategoryTheory.instIsIsoIndCoimageImageComparison : ∀ {C : Type v} [inst : CategoryTheory.SmallCategory C] [inst_1 : CategoryTheory.Abelian C] {X Y : CategoryTheory.Ind C}
  (f : X ⟶ Y), CategoryTheory.IsIso (CategoryTheory.Abelian.coimageImageComparison f)
-- Mathlib.Data.Int.Lemmas
Int.strictAntiOn_natAbs : StrictAntiOn Int.natAbs (Set.Iic 0)
-- Mathlib.Algebra.Lie.BaseChange
LieAlgebra.ExtendScalars.instBaseLieAlgebra : (R : Type u_1) →
  (A : Type u_2) →
    (L : Type u_3) →
      [inst : CommRing R] →
        [inst_1 : CommRing A] →
          [inst_2 : Algebra R A] → [inst_3 : LieRing L] → [inst_4 : LieAlgebra R L] → LieAlgebra R (TensorProduct R A L)
-- Mathlib.CategoryTheory.EquivalenceRelation
/-- `c` is limiting  -/
CategoryTheory.TransitiveRelation.isLimit : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {R X : C} →
      {p₁ p₂ : R ⟶ X} → (self : CategoryTheory.TransitiveRelation p₁ p₂) → CategoryTheory.Limits.IsLimit self.c
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
/-- Enables notation `xₖ : R[x₁, ..., xₙ]` instead of
`(⟨xₖ, "membership proof"⟩ : R[x₁, ..., xₙ])`.  -/
Algebra.instCoeDepSubtypeMemSubalgebraAdjoinOfCoeAdjoinAux : {A : Type u_2} →
  {B : Type u_3} →
    [inst : CommSemiring A] →
      [inst_1 : Semiring B] →
        [inst_2 : Algebra A B] → (s : Set B) → (x : B) → [Algebra.CoeAdjoinAux x s] → CoeDep B x ↥(Algebra.adjoin A s)
-- Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
MeasureTheory.integrable_rnDeriv_mul_log_iff : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ]
  [μ.HaveLebesgueDecomposition ν],
  μ.AbsolutelyContinuous ν →
    (MeasureTheory.Integrable (fun a => (μ.rnDeriv ν a).toReal * Real.log (μ.rnDeriv ν a).toReal) ν ↔
      MeasureTheory.Integrable (MeasureTheory.llr μ ν) μ)
-- Mathlib.Tactic.Abel
Mathlib.Tactic.Abel.zero_termg : ∀ {α : Type u_1} [inst : AddCommGroup α] (x a : α), Mathlib.Tactic.Abel.termg 0 x a = a
-- Mathlib.Topology.Covering.Quotient
Topology.IsQuotientMap.trivializationOfSMulDisjoint_target : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {f : E → X} {G : Type u_3}
  [inst_2 : Group G] [inst_3 : MulAction G E] (hf : Topology.IsQuotientMap f) [inst_4 : ContinuousConstSMul G E]
  (hfG : ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ MulAction.orbit G e₂) [inst_5 : TopologicalSpace G]
  [inst_6 : DiscreteTopology G] (U : Set E) (open_U : IsOpen U)
  (disjoint : ∀ (g : G), ((fun x => g • x) '' U ∩ U).Nonempty → g = 1),
  (hf.trivializationOfSMulDisjoint hfG U open_U disjoint).target = (f '' U) ×ˢ Set.univ
-- Mathlib.Data.Set.Lattice
/-- An equality version of this lemma is `iUnion_iInter_of_monotone` in `Data.Set.Finite`.  -/
Set.iUnion_iInter_subset : ∀ {α : Type u_1} {ι : Sort u_5} {ι' : Sort u_6} {s : ι → ι' → Set α}, ⋃ j, ⋂ i, s i j ⊆ ⋂ i, ⋃ j, s i j
-- Mathlib.Topology.Algebra.FilterBasis
GroupFilterBasis.N.eq_1 : ∀ {G : Type u} [inst : Group G] (B : GroupFilterBasis G) (x : G), B.N x = Filter.map (fun y => x * y) B.filter
-- Std.Time.Zoned.Database.TzIf
/-- The version of the TZif file format.
 -/
Std.Time.TimeZone.TZif.Header.version : Std.Time.TimeZone.TZif.Header → UInt8
-- Mathlib.Algebra.Module.Torsion.Free
IsRegular.smul_right_injective : ∀ {R : Type u_1} (M : Type u_3) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {r : R}
  [Module.IsTorsionFree R M], IsRegular r → Function.Injective fun x => r • x
-- Mathlib.AlgebraicTopology.SimplicialSet.NerveCodiscrete
/-- If a type `X` has decidable equality, the nerve of the codiscrete category on `X`
has decidable equality as well.  -/
CategoryTheory.Codiscrete.instDecidableEqObjOppositeSimplexCategoryNerveOpMk : {X : Type u} →
  {n : ℕ} →
    [DecidableEq X] → DecidableEq ((CategoryTheory.nerve (CategoryTheory.Codiscrete X)).obj (Opposite.op { len := n }))
-- Mathlib.RepresentationTheory.Homological.Resolution
Rep.barComplex.d_def : ∀ (k G : Type u) [inst : CommRing k] {n : ℕ} [inst_1 : Group G],
  (Rep.barComplex k G).d (n + 1) n = Rep.barComplex.d k G n
-- Mathlib.Tactic.Linter.TextBased
/-- The contexts describe different errors: two separate style exceptions are required
to cover both.  -/
_private.Mathlib.Tactic.Linter.TextBased.0.Mathlib.Linter.TextBased.ComparisonResult.Different : Mathlib.Linter.TextBased.ComparisonResult✝
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
ModelWithCorners.isInvertible_fderivWithin_extendCoordChange : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  {n : WithTop ℕ∞} {I : ModelWithCorners 𝕜 E H} {e e' : OpenPartialHomeomorph M H} [inst_5 : ChartedSpace H M],
  n ≠ 0 →
    e ∈ IsManifold.maximalAtlas I n M →
      e' ∈ IsManifold.maximalAtlas I n M →
        ∀ {x : E},
          x ∈ (ModelWithCorners.extendCoordChange e e').source →
            (fderivWithin 𝕜 (↑(ModelWithCorners.extendCoordChange e e'))
                (ModelWithCorners.extendCoordChange e e').source x).IsInvertible
-- Mathlib.LinearAlgebra.Matrix.ToLin
/-- If `M` and `M'` are each other's inverse matrices, they provide an equivalence between `m → A`
and `n → A` corresponding to `M.mulVec` and `M'.mulVec`.  -/
Matrix.toLin'OfInv : {R : Type u_1} →
  [inst : CommSemiring R] →
    {m : Type u_4} →
      {n : Type u_5} →
        [inst_1 : DecidableEq n] →
          [inst_2 : Fintype n] →
            [inst_3 : Fintype m] →
              [inst_4 : DecidableEq m] →
                {M : Matrix m n R} → {M' : Matrix n m R} → M * M' = 1 → M' * M = 1 → (m → R) ≃ₗ[R] n → R
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.size_alter_eq_self_of_not_mem : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} [inst_2 : LawfulBEq α]
  {k : α} {f : Option (β k) → Option (β k)}, m.WF → k ∉ m → (f (m.get? k)).isNone = true → (m.alter k f).size = m.size
-- Mathlib.Algebra.EuclideanDomain.Defs
EuclideanDomain.xgcdAux.eq_1 : ∀ {R : Type u} [inst : EuclideanDomain R] [inst_1 : DecidableEq R] (r s t r' s' t' : R),
  EuclideanDomain.xgcdAux r s t r' s' t' =
    if _hr : r = 0 then (r', s', t')
    else
      have q := r' / r;
      have x := ⋯;
      EuclideanDomain.xgcdAux (r' % r) (s' - q * s) (t' - q * t) r s t
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.InternalState.urls : Lean.Doc.InternalState → Std.HashMap String (Lean.Doc.Ref✝ String)
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.mem_map_equiv : ∀ {N : Type u_2} [inst : MulOneClass N] {M : Type u_5} [inst_1 : MulOneClass M] {f : M ≃* N} {K : Submonoid M} {x : N},
  x ∈ Submonoid.map f.toMonoidHom K ↔ f.symm x ∈ K
-- Mathlib.LinearAlgebra.Alternating.Basic
MultilinearMap.alternatization_def : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N' : Type u_6}
  [inst_3 : AddCommGroup N'] [inst_4 : Module R N'] {ι : Type u_7} [inst_5 : Fintype ι] [inst_6 : DecidableEq ι]
  (m : MultilinearMap R (fun x => M) N'),
  ⇑(MultilinearMap.alternatization m) = ⇑(∑ σ, Equiv.Perm.sign σ • MultilinearMap.domDomCongr σ m)
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.ToCodeBlock.ToForInTermResult : Type
-- Mathlib.Order.Category.Lat
Lat.str : (self : Lat) → Lattice ↑self
-- Mathlib.Data.Set.Prod
Set.prod_eq_empty_iff : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β}, s ×ˢ t = ∅ ↔ s = ∅ ∨ t = ∅
-- Mathlib.Algebra.Group.Subsemigroup.Defs
Subsemigroup.instNontrivialOfNonempty : ∀ {M : Type u_1} [inst : Mul M] [hn : Nonempty M], Nontrivial (Subsemigroup M)
-- Std.Time.Format.Modifier
/-- `w`: Week of week-based year (e.g., 27).
 -/
Std.Time.Modifier.w : Std.Time.Number → Std.Time.Modifier
-- Mathlib.Topology.Instances.EReal.Lemmas
EReal.tendsto_coe : ∀ {α : Type u_2} {f : Filter α} {m : α → ℝ} {a : ℝ},
  Filter.Tendsto (fun a => ↑(m a)) f (nhds ↑a) ↔ Filter.Tendsto m f (nhds a)
-- Mathlib.Combinatorics.SimpleGraph.Basic
/-- All vertices are in the support of the complete graph if there is more than one vertex.  -/
SimpleGraph.support_top_of_nontrivial : ∀ {V : Type u} [Nontrivial V], ⊤.support = Set.univ
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
ContinuousLinearMapWOT.instSMul : {𝕜₁ : Type u_1} →
  {𝕜₂ : Type u_2} →
    [inst : NormedField 𝕜₁] →
      [inst_1 : NormedField 𝕜₂] →
        {σ : 𝕜₁ →+* 𝕜₂} →
          {E : Type u_3} →
            {F : Type u_4} →
              [inst_2 : AddCommGroup E] →
                [inst_3 : TopologicalSpace E] →
                  [inst_4 : Module 𝕜₁ E] →
                    [inst_5 : AddCommGroup F] →
                      [inst_6 : TopologicalSpace F] →
                        [inst_7 : Module 𝕜₂ F] →
                          {S : Type u_5} →
                            [inst_8 : DistribSMul S F] →
                              [SMulCommClass 𝕜₂ S F] → [ContinuousConstSMul S F] → SMul S (E →SWOT[σ] F)
-- Mathlib.LinearAlgebra.Dual.Lemmas
Submodule.dualCopairing_eq : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (W : Submodule R M),
  W.dualCopairing = ↑W.dualQuotEquivDualAnnihilator.symm
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
/-- The composition of left homology map data.  -/
CategoryTheory.ShortComplex.LeftHomologyMapData.comp : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S₁ S₂ S₃ : CategoryTheory.ShortComplex C} →
        {φ : S₁ ⟶ S₂} →
          {φ' : S₂ ⟶ S₃} →
            {h₁ : S₁.LeftHomologyData} →
              {h₂ : S₂.LeftHomologyData} →
                {h₃ : S₃.LeftHomologyData} →
                  CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂ →
                    CategoryTheory.ShortComplex.LeftHomologyMapData φ' h₂ h₃ →
                      CategoryTheory.ShortComplex.LeftHomologyMapData (CategoryTheory.CategoryStruct.comp φ φ') h₁ h₃
-- Std.Data.DTreeMap.Internal.Lemmas
_private.Std.Data.DTreeMap.Internal.Lemmas.0.Std.DTreeMap.Internal.Impl.modifyMap : Std.HashMap Lean.Name Lean.Name
-- Mathlib.Analysis.BoxIntegral.UnitPartition
_private.Mathlib.Analysis.BoxIntegral.UnitPartition.0.BoxIntegral.unitPartition.mem_admissibleIndex_of_mem_box_aux₂ : ∀ (n : ℕ) [NeZero n] (x : ℝ) (a : ℤ), x ≤ ↑a ↔ (↑⌈↑n * x⌉ - 1 + 1) / ↑n ≤ ↑a
-- Std.Data.DTreeMap.AdditionalOperations
/-- Given a proof that such a mapping exists, retrieves the key-value pair with the largest key that is
less than or equal to the given key.
 -/
Std.DTreeMap.getEntryLE : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} →
      [Std.TransCmp cmp] → (t : Std.DTreeMap α β cmp) → (k : α) → (∃ a ∈ t, (cmp a k).isLE = true) → (a : α) × β a
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.maxKeyD_alterKey_eq_self : ∀ {α : Type u} {β : Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {l : List ((_ : α) × β)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k : α} {f : Option β → Option β},
      (Std.Internal.List.Const.alterKey k f l).isEmpty = false →
        ∀ {fallback : α},
          Std.Internal.List.maxKeyD (Std.Internal.List.Const.alterKey k f l) fallback = k ↔
            (f (Std.Internal.List.getValue? k l)).isSome = true ∧
              ∀ (k' : α), Std.Internal.List.containsKey k' l = true → (compare k' k).isLE = true
-- Mathlib.Data.Finset.BooleanAlgebra
Finset.univ_val_map_subtype_val : ∀ {α : Type u_1} [inst : Fintype α] (p : α → Prop) [inst_1 : DecidablePred p] [inst_2 : Fintype { a // p a }],
  Multiset.map Subtype.val Finset.univ.val = (Finset.filter p Finset.univ).val
-- Mathlib.Analysis.Normed.Lp.Matrix
Matrix.toLpLin_apply : ∀ {m : Type u_1} {n : Type u_2} {R : Type u_4} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing R]
  (p q : ENNReal) (M : Matrix m n R) (v : WithLp p (n → R)),
  ((Matrix.toLpLin p q) M) v = WithLp.toLp q (M.mulVec v.ofLp)
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.right_vsub_lineMap : ∀ {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V1] [inst_2 : Module k V1]
  [inst_3 : AddTorsor V1 P1] (p₀ p₁ : P1) (c : k), p₁ -ᵥ (AffineMap.lineMap p₀ p₁) c = (1 - c) • (p₁ -ᵥ p₀)
-- Mathlib.CategoryTheory.Whiskering
/-- If `F : D ⥤ E` is fully faithful, then so is
`(whiskeringRight C D E).obj F : (C ⥤ D) ⥤ C ⥤ E`.  -/
CategoryTheory.Functor.FullyFaithful.whiskeringRight : {D : Type u₂} →
  [inst : CategoryTheory.Category.{v₂, u₂} D] →
    {E : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} E] →
        {F : CategoryTheory.Functor D E} →
          F.FullyFaithful →
            (C : Type u_1) →
              [inst_2 : CategoryTheory.Category.{v_1, u_1} C] →
                ((CategoryTheory.Functor.whiskeringRight C D E).obj F).FullyFaithful
-- Mathlib.Data.ENNReal.Operations
ENNReal.iInf_gt_eq_self : ∀ (a : ENNReal), ⨅ b, ⨅ (_ : a < b), b = a
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.vadd_subset_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : VAdd α β] {s : Set α} {t u : Set β}, s +ᵥ t ⊆ u ↔ ∀ a ∈ s, ∀ b ∈ t, a +ᵥ b ∈ u
-- Mathlib.Algebra.Group.Submonoid.Units
Submonoid.val_unitsEquivUnitsType_symm_apply_coe : ∀ {M : Type u_1} [inst : Monoid M] (S : Submonoid M) (x : (↥S)ˣ), ↑↑(S.unitsEquivUnitsType.symm x) = ↑↑x
-- Mathlib.Analysis.Fourier.AddCircle
fourierCoeff.const_mul : ∀ {T : ℝ} [hT : Fact (0 < T)] (f : AddCircle T → ℂ) (c : ℂ) (n : ℤ),
  fourierCoeff (fun x => c * f x) n = c * fourierCoeff f n
-- Mathlib.Algebra.Quandle
Rack.PreEnvelGroupRel'.congr_mul.inj : ∀ {R : Type u} {inst : Rack R} {a b a' b' : Rack.PreEnvelGroup R} {ha : Rack.PreEnvelGroupRel' R a a'}
  {hb : Rack.PreEnvelGroupRel' R b b'} {ha_1 : Rack.PreEnvelGroupRel' R a a'} {hb_1 : Rack.PreEnvelGroupRel' R b b'},
  ha.congr_mul hb = ha_1.congr_mul hb_1 → ha = ha_1 ∧ hb = hb_1
-- Mathlib.Logic.Encodable.Basic
/-- Decoding from ℕ to Option α  -/
Encodable.decode : {α : Type u_1} → [self : Encodable α] → ℕ → Option α
-- Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy
HomotopicalAlgebra.CofibrantObject.toHoCat_map_eq_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.ModelCategory C]
  {X Y : HomotopicalAlgebra.CofibrantObject C} [HomotopicalAlgebra.IsFibrant Y.obj] (f g : X ⟶ Y),
  HomotopicalAlgebra.CofibrantObject.toHoCat.map f = HomotopicalAlgebra.CofibrantObject.toHoCat.map g ↔
    HomotopicalAlgebra.CofibrantObject.homRel C f g
-- Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
FreeGroup.IsCyclicallyReduced.isReduced : ∀ {α : Type u} {L : List (α × Bool)}, FreeGroup.IsCyclicallyReduced L → FreeGroup.IsReduced L
-- Init.Data.String.Defs
String.startInclusive_toSlice : ∀ {s : String}, s.toSlice.startInclusive = s.startPos
-- Mathlib.Algebra.Order.Monovary
/-- **Alias** of the reverse direction of `monovaryOn_inv₀`. -/
MonovaryOn.inv₀ : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Semifield α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α]
  [inst_3 : Semifield β] [inst_4 : LinearOrder β] [IsStrictOrderedRing β] {s : Set ι} {f : ι → α} {g : ι → β},
  (∀ i ∈ s, 0 < f i) → (∀ i ∈ s, 0 < g i) → MonovaryOn f g s → MonovaryOn f⁻¹ g⁻¹ s
-- Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
IsBoundedLinearMap.bound : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : Semiring 𝕜] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : Module 𝕜 E] [inst_3 : SeminormedAddCommGroup F] [inst_4 : Module 𝕜 F] {f : E → F},
  IsBoundedLinearMap 𝕜 f → ∃ M, 0 < M ∧ ∀ (x : E), ‖f x‖ ≤ M * ‖x‖
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.isBigO_const_const_iff : ∀ {α : Type u_1} {E'' : Type u_9} {F'' : Type u_10} [inst : NormedAddCommGroup E''] [inst_1 : NormedAddCommGroup F'']
  {c : E''} {c' : F''} (l : Filter α) [l.NeBot], ((fun _x => c) =O[l] fun _x => c') ↔ c' = 0 → c = 0
-- Mathlib.Analysis.Normed.Group.Seminorm
GroupSeminorm.sSup_of_not_bddAbove : ∀ {E : Type u_3} [inst : Group E] {s : Set (GroupSeminorm E)}, ¬BddAbove s → sSup s = 0
-- Lean.Data.Lsp.InitShutdown
Lean.Lsp.ClientInfo.name : Lean.Lsp.ClientInfo → String
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.presieve₀_mem_iff_of_iso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} [J.RespectsIso] {S : C}
  {E F : CategoryTheory.PreZeroHypercover S} (e : E ≅ F), E.presieve₀ ∈ J.coverings S ↔ F.presieve₀ ∈ J.coverings S
-- Std.Data.HashMap.Lemmas
Std.HashMap.isSome_getKey?_iff_mem : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {a : α}, (m.getKey? a).isSome = true ↔ a ∈ m
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.maxKey!_insert : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {k : α} {v : β},
  (t.insert k v).maxKey! = t.maxKey?.elim k fun k' => if (cmp k' k).isLE = true then k else k'
-- Batteries.Data.Array.Basic
/-- Folds a monadic function over an array from the right, accumulating the partial results starting
with `init`. The accumulated value is combined with the each element of the list in order using `f`.

The optional parameters `start` and `stop` control the region of the array to be folded. Folding
proceeds from `start` (exclusive) to `stop` (inclusive), so no folding occurs unless `start > stop`.
By default, the entire array is folded.

Examples:
```lean example
example [Monad m] (f : α → β → m β) :
    Array.scanrM f x₀ #[a, b, c] = (do
      let x₁ ← f c x₀
      let x₂ ← f b x₁
      let x₃ ← f a x₂
      pure #[x₃, x₂, x₁, x₀])
    := by simp [scanrM, scanrM.loop]
```

```lean example
example [Monad m] (f : α → β → m β) :
    Array.scanrM f x₀ #[a, b, c] (start := 3) (stop := 1) = (do
      let x₁ ← f c x₀
      let x₂ ← f b x₁
      pure #[x₂, x₁, x₀])
    := by simp [scanrM, scanrM.loop]
```
 -/
Array.scanrM : {m : Type u_1 → Type u_2} →
  {α : Type u_3} →
    {β : Type u_1} → [Monad m] → (α → β → m β) → β → (as : Array α) → optParam ℕ as.size → optParam ℕ 0 → m (Array β)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.Functor.OplaxMonoidal.lift_δ_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  (F : CategoryTheory.Functor C D) {X Y Z : C} [inst_4 : F.OplaxMonoidal] (f : X ⟶ Y) (g : X ⟶ Z) {Z_1 : D}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj (F.obj Y) (F.obj Z) ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.CartesianMonoidalCategory.lift f g))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.δ F Y Z) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift (F.map f) (F.map g)) h
-- Mathlib.Topology.Connected.PathConnected
joinedIn_iff_joined : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X} {F : Set X} (x_in : x ∈ F) (y_in : y ∈ F),
  JoinedIn F x y ↔ Joined ⟨x, x_in⟩ ⟨y, y_in⟩
-- Mathlib.Algebra.Homology.BifunctorShift
CategoryTheory.Functor.instCommShiftCochainComplexIntObjMap₂CochainComplex : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {D : Type u_3} →
      [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} D] →
            [inst_3 : CategoryTheory.Preadditive C₁] →
              [inst_4 : CategoryTheory.Preadditive C₂] →
                [inst_5 : CategoryTheory.Preadditive D] →
                  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) →
                    [inst_6 : F.Additive] →
                      [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).Additive] →
                        [inst_8 : ∀ (K₁ : CochainComplex C₁ ℤ) (K₂ : CochainComplex C₂ ℤ), K₁.HasMapBifunctor K₂ F] →
                          (K₁ : CochainComplex C₁ ℤ) → (F.map₂CochainComplex.obj K₁).CommShift ℤ
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.lift_mk_le_lift_mk_of_injective : ∀ {α : Type u} {β : Type v} {f : α → β},
  Function.Injective f → Cardinal.lift.{v, u} (Cardinal.mk α) ≤ Cardinal.lift.{u, v} (Cardinal.mk β)
-- Lean.Parser.Types
Lean.Parser.ParserState.shrinkStack : Lean.Parser.ParserState → ℕ → Lean.Parser.ParserState