mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Group.Arithmetic
Finset.measurable_fun_sum : ∀ {M : Type u_2} {ι : Type u_3} {α : Type u_4} [inst : AddCommMonoid M] [inst_1 : MeasurableSpace M] [MeasurableAdd₂ M]
  {m : MeasurableSpace α} {f : ι → α → M} (s : Finset ι),
  (∀ i ∈ s, Measurable (f i)) → Measurable fun a => ∑ i ∈ s, f i a
-- Mathlib.Logic.Equiv.Defs
Equiv.exists_congr' : ∀ {α : Sort u} {β : Sort v} {p : α → Prop} {q : β → Prop} (e : α ≃ β),
  (∀ (b : β), p (e.symm b) ↔ q b) → ((∃ a, p a) ↔ ∃ b, q b)
-- Mathlib.CategoryTheory.Bicategory.InducedBicategory
CategoryTheory.Bicategory.InducedBicategory.forget_mapId_inv : ∀ {B : Type u_1} {C : Type u_2} [inst : CategoryTheory.Bicategory C] {F : B → C}
  (x : CategoryTheory.Bicategory.InducedBicategory C F),
  (CategoryTheory.Bicategory.InducedBicategory.forget.mapId x).inv =
    CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.id (F x))
-- Mathlib.Algebra.GradedMulAction
SetLike.GradedSMul.mk : ∀ {ιA : Type u_1} {ιB : Type u_2} {S : Type u_5} {R : Type u_6} {N : Type u_7} {M : Type u_8} [inst : SetLike S R]
  [inst_1 : SetLike N M] [inst_2 : SMul R M] [inst_3 : VAdd ιA ιB] {A : ιA → S} {B : ιB → N},
  (∀ ⦃i : ιA⦄ ⦃j : ιB⦄ {ai : R} {bj : M}, ai ∈ A i → bj ∈ B j → ai • bj ∈ B (i +ᵥ j)) → SetLike.GradedSMul A B
-- Mathlib.MeasureTheory.Integral.Bochner.L1
MeasureTheory.SimpleFunc.integral_eq_sum_filter : ∀ {α : Type u_1} {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F]
  [inst_2 : DecidablePred fun x => x ≠ 0] {m : MeasurableSpace α} (f : MeasureTheory.SimpleFunc α F)
  (μ : MeasureTheory.Measure α),
  MeasureTheory.SimpleFunc.integral μ f = ∑ x ∈ f.range with x ≠ 0, μ.real (⇑f ⁻¹' {x}) • x
-- Mathlib.Tactic.Translate.Core
/-- When `isDual := true`, every translation `A → B` will also give a translation `B → A`.  -/
Mathlib.Tactic.Translate.TranslateData.isDual : Mathlib.Tactic.Translate.TranslateData → Bool
-- Mathlib.RingTheory.LocalRing.Defs
IsLocalRing.of_is_unit_or_is_unit_of_add_one : ∀ {R : Type u_1} [inst : Semiring R] [toNontrivial : Nontrivial R],
  (∀ {a b : R}, a + b = 1 → IsUnit a ∨ IsUnit b) → IsLocalRing R
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.mem_range_coroot_of_mem_range_coreflection_of_mem_range_coroot : ∀ {ι : 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) {r : N ≃ₗ[R] N}
  {α : N}, r ∈ Set.range P.coreflection → α ∈ Set.range ⇑P.coroot → r • α ∈ Set.range ⇑P.coroot
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.LaxBraidedFunctor.homMk_hom_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {D : Type u₂} [inst_3 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_4 : CategoryTheory.MonoidalCategory D] [inst_5 : CategoryTheory.BraidedCategory D]
  {F G : CategoryTheory.LaxBraidedFunctor C D} (f : F.toFunctor ⟶ G.toFunctor)
  [inst_6 : CategoryTheory.NatTrans.IsMonoidal f], (CategoryTheory.LaxBraidedFunctor.homMk f).hom.hom = f
-- Init.Data.String.Modify
/-- Replaces the character at position `p` in the string `s` with the result of applying `f` to that
character.

If both the replacement character and the replaced character are 7-bit ASCII characters and the
string is not shared, then it is updated in-place and not copied.

Examples:
* `("abc".pos ⟨1⟩ (by decide)).modify Char.toUpper (by decide) = "aBc"`
 -/
String.Pos.modify : {s : String} → (p : s.Pos) → (Char → Char) → p ≠ s.endPos → String
-- Init.Data.String.Basic
String.Slice.Pos.offset_str : ∀ {s : String.Slice} {pos : s.Pos}, pos.str.offset = pos.offset.offsetBy s.startInclusive.offset
-- Mathlib.Data.PNat.Factors
PrimeMultiset.to_ofNatMultiset : ∀ (v : Multiset ℕ) (h : ∀ p ∈ v, Nat.Prime p), (PrimeMultiset.ofNatMultiset v h).toNatMultiset = v
-- Mathlib.Topology.Algebra.RestrictedProduct.Units
RestrictedProduct.isUnit_iff : ∀ {ι : Type u_1} {R : ι → Type u_2} [inst : (i : ι) → Monoid (R i)] {S : ι → Type u_3}
  [inst_1 : (i : ι) → SetLike (S i) (R i)] [inst_2 : ∀ (i : ι), SubmonoidClass (S i) (R i)] {B : (i : ι) → S i}
  {𝓕 : Filter ι} {x : RestrictedProduct (fun i => R i) (fun i => ↑(B i)) 𝓕},
  IsUnit x ↔ (∀ (i : ι), IsUnit (x i)) ∧ ∀ᶠ (i : ι) in 𝓕, ∃ (h : x i ∈ B i), IsUnit ⟨x i, h⟩
-- Mathlib.RingTheory.RingHom.Flat
Algebra.TensorProduct.mapOfCompatibleSMul.congr_simp : ∀ (R : Type u_3) (S : Type u_4) (T : Type u_5) (A : Type u_6) (B : Type u_7) [inst : CommSemiring R]
  [inst_1 : CommSemiring S] [inst_2 : CommSemiring T] [inst_3 : Semiring A] [inst_4 : Semiring B] [inst_5 : Algebra R A]
  [inst_6 : Algebra R B] [inst_7 : Algebra S A] [inst_8 : Algebra S B] [inst_9 : Algebra T A]
  [inst_10 : SMulCommClass R T A] [inst_11 : SMulCommClass S T A] [inst_12 : SMulCommClass R S A]
  [inst_13 : TensorProduct.CompatibleSMul R S A B],
  Algebra.TensorProduct.mapOfCompatibleSMul R S T A B = Algebra.TensorProduct.mapOfCompatibleSMul R S T A B
-- Mathlib.MeasureTheory.Measure.Haar.Basic
MeasureTheory.Measure.haar.eq_1 : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalGroup G]
  [inst_3 : MeasurableSpace G] [inst_4 : BorelSpace G] [inst_5 : LocallyCompactSpace G],
  MeasureTheory.Measure.haar =
    MeasureTheory.Measure.haarMeasure (Classical.arbitrary (TopologicalSpace.PositiveCompacts G))
-- Mathlib.CategoryTheory.Limits.Types.ColimitType
/-- Given `F : J ⥤ Type w₀` and `c : F.CoconeTypes`, this is the property
that `c` is a colimit. It is defined by saying the canonical map
`F.descColimitType c : F.ColimitType → c.pt` is a bijection.  -/
CategoryTheory.Functor.CoconeTypes.IsColimit : {J : Type u} →
  [inst : CategoryTheory.Category.{v, u} J] → {F : CategoryTheory.Functor J (Type w₀)} → F.CoconeTypes → Prop
-- Mathlib.Topology.Algebra.Module.FiniteDimension
LinearEquiv.canLiftContinuousLinearEquiv : ∀ {𝕜 : Type u} [hnorm : NontriviallyNormedField 𝕜] {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E]
  [inst_2 : TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] {F : Type w} [inst_5 : AddCommGroup F]
  [inst_6 : Module 𝕜 F] [inst_7 : TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousSMul 𝕜 F] [CompleteSpace 𝕜]
  [T2Space E] [T2Space F] [FiniteDimensional 𝕜 E],
  CanLift (E ≃ₗ[𝕜] F) (E ≃L[𝕜] F) ContinuousLinearEquiv.toLinearEquiv fun x => True
-- Mathlib.Data.Fin.Tuple.Finset
Finset.map_insertNthEquiv_filter_piFinset : ∀ {n : ℕ} {α : Fin (n + 1) → Type u_1} {p : Fin (n + 1)} (S : (i : Fin (n + 1)) → Finset (α i))
  (P : ((i : Fin n) → α (p.succAbove i)) → Prop) [inst : DecidablePred P],
  Finset.map (Fin.insertNthEquiv α p).symm.toEmbedding ({r ∈ Fintype.piFinset S | P (p.removeNth r)}) =
    S p ×ˢ {r ∈ Fintype.piFinset (p.removeNth S) | P r}
-- Mathlib.MeasureTheory.Group.LIntegral
MeasureTheory.lintegral_div_left_eq_self : ∀ {G : Type u_1} [inst : MeasurableSpace G] {μ : MeasureTheory.Measure G} [inst_1 : Group G] [MeasurableMul G]
  [μ.IsMulLeftInvariant] [MeasurableInv G] [μ.IsInvInvariant] (f : G → ENNReal) (g : G),
  ∫⁻ (x : G), f (g / x) ∂μ = ∫⁻ (x : G), f x ∂μ
-- Mathlib.Algebra.Category.Grp.Yoneda
AddCommGrpCat.coyonedaForget.eq_1 : AddCommGrpCat.coyonedaForget =
  CategoryTheory.NatIso.ofComponents
    (fun X =>
      CategoryTheory.NatIso.ofComponents
        (fun Y =>
          { hom := TypeCat.ofHom fun f => AddCommGrpCat.ofHom f, inv := TypeCat.ofHom fun f => AddCommGrpCat.Hom.hom f,
            hom_inv_id := ⋯, inv_hom_id := ⋯ })
        ⋯)
    @AddCommGrpCat.coyonedaForget._proof_4
-- Mathlib.ModelTheory.Algebra.Field.Basic
FirstOrder.Field.FieldAxiom.leftDistrib.sizeOf_spec : sizeOf FirstOrder.Field.FieldAxiom.leftDistrib = 1
-- Mathlib.RingTheory.LinearDisjoint
Subalgebra.LinearDisjoint.inf_eq_bot : ∀ {R : Type u} {S : Type v} [inst : Field R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {A B : Subalgebra R S},
  A.LinearDisjoint B → A ⊓ B = ⊥
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
CochainComplex.mappingCone.descCocycle.congr_simp : ∀ {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 ℤ}
  {n m : ℤ} (α α_1 : CochainComplex.HomComplex.Cochain F K m) (e_α : α = α_1)
  (β β_1 : CochainComplex.HomComplex.Cocycle G K n) (e_β : β = β_1) (h : m + 1 = n)
  (eq : CochainComplex.HomComplex.δ m n α = n.negOnePow • (CochainComplex.HomComplex.Cochain.ofHom φ).comp ↑β ⋯),
  CochainComplex.mappingCone.descCocycle φ α β h eq = CochainComplex.mappingCone.descCocycle φ α_1 β_1 h ⋯
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Lemmas
/-- performRupAdd adds to f.rupUnits and then clears f.rupUnits. If f begins with some units in f.rupUnits,
then performRupAdd will clear more than it intended to which will break the correctness of rupAdd_result.
 -/
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.ReadyForRupAdd : {n : ℕ} → Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n → Prop
-- Mathlib.Algebra.SkewMonoidAlgebra.Lift
SkewMonoidAlgebra.liftNCRingHom.eq_1 : ∀ {k : Type u_1} {G : Type u_2} [inst : Semiring k] [inst_1 : Monoid G] [inst_2 : MulSemiringAction G k] {R : Type u_3}
  [inst_3 : Semiring R] (f : k →+* R) (g : G →* R) (h_comm : ∀ {x : k} {y : G}, f (y • x) * g y = g y * f x),
  SkewMonoidAlgebra.liftNCRingHom f g h_comm =
    { toFun := (↑(SkewMonoidAlgebra.liftNC ↑f ⇑g)).toFun, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.imp_elim' : ∀ {σs : List (Type u)} {P Q R : Std.Do.SPred σs}, (Q ⊢ₛ P → R) → P ∧ Q ⊢ₛ R
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Ideal.IsHomogeneous.toIdeal_homogeneousCore_eq_self : ∀ {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [inst : Semiring A] [inst_1 : SetLike σ A]
  [inst_2 : AddSubmonoidClass σ A] {𝒜 : ι → σ} [inst_3 : DecidableEq ι] [inst_4 : AddMonoid ι] [inst_5 : GradedRing 𝒜]
  {I : Ideal A}, Ideal.IsHomogeneous 𝒜 I → (Ideal.homogeneousCore 𝒜 I).toIdeal = I
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
/-- **Alias** of `Submodule.coe_orthogonalProjectionOnto_apply`. -/
Submodule.coe_orthogonalProjection_apply : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (U : Submodule 𝕜 E) [inst_3 : U.HasOrthogonalProjection] (v : E), ↑(U.orthogonalProjectionOnto v) = U.starProjection v
-- Mathlib.Algebra.Group.Submonoid.Saturation
SaturatedSubmonoid.instCompleteSemilatticeInf : (M : Type u_1) → [inst : MulOneClass M] → CompleteSemilatticeInf (SaturatedSubmonoid M)
-- Mathlib.GroupTheory.Coprod.Basic
Monoid.Coprod.swap_comp_inr : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N],
  (Monoid.Coprod.swap M N).comp Monoid.Coprod.inr = Monoid.Coprod.inl
-- Mathlib.Data.Fintype.Order
Fin.completeLinearOrder : {n : ℕ} → [NeZero n] → CompleteLinearOrder (Fin n)
-- Mathlib.Data.Set.Basic
Set.mem_union_right : ∀ {α : Type u} {x : α} {b : Set α} (a : Set α), x ∈ b → x ∈ a ∪ b
-- Mathlib.Data.TypeVec
instInhabitedTypeVec : {n : ℕ} → Inhabited (TypeVec.{u} n)
-- Mathlib.Order.BooleanAlgebra.Set
Set.compl_univ : ∀ {α : Type u_1}, Set.univᶜ = ∅
-- Init.Data.Int.DivMod.Lemmas
Int.neg_fmod_neg : ∀ (a b : ℤ), (-a).fmod (-b) = -a.fmod b
-- Init.Data.SInt.Lemmas
Int16.toNatClampNeg_ofBitVec : ∀ (b : BitVec 16), (Int16.ofBitVec b).toNatClampNeg = b.toInt.toNat
-- Mathlib.Topology.ContinuousMap.ContinuousSqrt
instContinuousSqrtRCLike : {𝕜 : Type u_1} → [inst : RCLike 𝕜] → ContinuousSqrt 𝕜
-- Init.Data.Iterators.Lemmas.Combinators.Take
_private.Init.Data.Iterators.Lemmas.Combinators.Take.0.Std.Iter.atIdxSlow?_eq_match.match_1.splitter : (motive : ℕ → Sort u_1) → (n : ℕ) → (Unit → motive 0) → ((n : ℕ) → motive n.succ) → motive n
-- Std.Data.DTreeMap.Internal.Queries
/-- Implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.Const.getEntryLTD : {α : Type u} → {β : Type v} → [Ord α] → α → (Std.DTreeMap.Internal.Impl α fun x => β) → α × β → α × β
-- Mathlib.Analysis.Calculus.FDeriv.Congr
Filter.EventuallyEq.fderivWithin : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f f₁ : E → F} {x : E} {s : Set E},
  f₁ =ᶠ[nhdsWithin x s] f → fderivWithin 𝕜 f₁ s =ᶠ[nhdsWithin x s] fderivWithin 𝕜 f s
-- Init.PropLemmas
/-- Excluded middle commuted.  Added as alias for Decidable.em  -/
Decidable.not_or_self : ∀ (p : Prop) [h : Decidable p], ¬p ∨ p
-- Mathlib.Probability.Process.Stopping
MeasureTheory.IsStoppingTime.max_const : ∀ {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : LinearOrder ι] {f : MeasureTheory.Filtration ι m}
  {τ : Ω → WithTop ι},
  MeasureTheory.IsStoppingTime f τ → ∀ (i : ι), MeasureTheory.IsStoppingTime f fun ω => max (τ ω) ↑i
-- Mathlib.GroupTheory.Goursat
AddSubgroup.goursatSnd.eq_1 : ∀ {G : Type u_1} {H : Type u_2} [inst : AddGroup G] [inst_1 : AddGroup H] (I : AddSubgroup (G × H)),
  I.goursatSnd = AddSubgroup.map ((AddMonoidHom.snd G H).comp I.subtype) ((AddMonoidHom.fst G H).comp I.subtype).ker
-- Mathlib.Geometry.Manifold.VectorField.Pullback
/-- The pullback of a `C^m` vector field by a `C^n` function with invertible derivative and
with `m + 1 ≤ n` is `C^m`.
Version within a set at a point, but with full pullback.  -/
ContMDiffWithinAt.mpullback_vectorField_preimage_of_eq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {H' : Type u_5} [inst_6 : TopologicalSpace H']
  {E' : Type u_6} [inst_7 : NormedAddCommGroup E'] [inst_8 : NormedSpace 𝕜 E'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {x₀ : M}
  {V : (x : M') → TangentSpace I' x} {m n : WithTop ℕ∞} {t : Set M'} {y₀ : M'} [CompleteSpace E]
  [inst_12 : IsManifold I 1 M] [inst_13 : IsManifold I' 1 M'],
  ContMDiffWithinAt I' I'.tangent m (fun x => ⟨x, V x⟩) t y₀ →
    ContMDiffAt I I' n f x₀ →
      (mfderiv% f x₀).IsInvertible →
        m + 1 ≤ n →
          y₀ = f x₀ → ContMDiffWithinAt I I.tangent m (fun x => ⟨x, VectorField.mpullback I I' f V x⟩) (f ⁻¹' t) x₀
-- Mathlib.Data.Multiset.Count
Multiset.count_attach : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Multiset α} (a : { x // x ∈ s }),
  Multiset.count a s.attach = Multiset.count (↑a) s
-- Mathlib.Algebra.Homology.LeftResolution.Reduced
CategoryTheory.Abelian.LeftResolution.instPreservesZeroMorphismsKaroubiF : ∀ {A : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_1} A] {ι : CategoryTheory.Functor C A}
  (Λ : CategoryTheory.Abelian.LeftResolution ι) [inst_2 : CategoryTheory.Preadditive C]
  [inst_3 : CategoryTheory.Preadditive A], (CategoryTheory.Abelian.LeftResolution.karoubi.F Λ).PreservesZeroMorphisms
-- Mathlib.Algebra.Group.Submonoid.Units
/-- The equivalence between the coercion of an additive subgroup `S` of
`Mˣ` to an additive submonoid of `M` and the additive subgroup itself as a type.  -/
AddSubgroup.ofAddUnitsEquivType : {M : Type u_1} → [inst : AddMonoid M] → (S : AddSubgroup (AddUnits M)) → ↥S.ofAddUnits ≃+ ↥S
-- Mathlib.CategoryTheory.Bicategory.Functor.Lax
/-- Lax right unity.  -/
CategoryTheory.LaxFunctor.map₂_rightUnitor_app_assoc : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] (self : CategoryTheory.LaxFunctor B CategoryTheory.Cat) {a b : B}
  (f : a ⟶ b) (X : ↑(self.obj a)) {Z : ↑(self.obj b)}
  (h : (self.map (CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.id b))).toFunctor.obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((self.map₂ (CategoryTheory.Bicategory.rightUnitor f).inv).toNatTrans.app X) h =
    CategoryTheory.CategoryStruct.comp ((self.mapId b).toNatTrans.app ((self.map f).toFunctor.obj X))
      (CategoryTheory.CategoryStruct.comp ((self.mapComp f (CategoryTheory.CategoryStruct.id b)).toNatTrans.app X) h)
-- Mathlib.Topology.Connected.PathConnected
/-- If a set `W` is path-connected, then it is also path-connected when seen as a set in a smaller
ambient type `U` (when `U` contains `W`).  -/
IsPathConnected.preimage_coe : ∀ {X : Type u_1} [inst : TopologicalSpace X] {U W : Set X},
  IsPathConnected W → W ⊆ U → IsPathConnected (Subtype.val ⁻¹' W)
-- Mathlib.Tactic.Linter.TextBased
/-- Lint a collection of input strings for disallowed unicode characters.

This is implemented using an allowlist, see
`Mathlib.Linter.TextBased.UnicodeLinter.isAllowedCharacter`.  -/
Mathlib.Linter.TextBased.linter.unicodeLinter : Lean.Option Bool
-- Mathlib.GroupTheory.Index
/-- The additive subgroup has finite index;
recall that `AddSubgroup.index` returns 0 when the index is infinite.  -/
AddSubgroup.FiniteIndex.index_ne_zero : ∀ {G : Type u_3} {inst : AddGroup G} {H : AddSubgroup G} [self : H.FiniteIndex], H.index ≠ 0
-- Mathlib.Order.KrullDimension
Order.coheight.eq_1 : ∀ {α : Type u_1} [inst : Preorder α] (a : α), Order.coheight a = Order.height a
-- Lean.HeadIndex
Lean.instHashableHeadIndex : Hashable Lean.HeadIndex
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.map₂_map_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {A : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} A] {B : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} B] {L : D} {R : CategoryTheory.Functor C D} {L' : B}
  {R' : CategoryTheory.Functor A B} {F : CategoryTheory.Functor C A} {G : CategoryTheory.Functor D B} (α : L' ⟶ G.obj L)
  (β : R.comp G ⟶ F.comp R') {X Y : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit L) R} (φ : X ⟶ Y),
  ((CategoryTheory.StructuredArrow.map₂ α β).map φ).left = CategoryTheory.CategoryStruct.id X.left
-- Mathlib.Data.Vector.MapLemmas
/-- If `f` takes a pair of states, but always returns the same value for both elements of the
pair, then we can simplify to just a single element of state.
 -/
List.Vector.mapAccumr₂_redundant_pair : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {σ : Type u_5} {n : ℕ} {s : σ} {xs : List.Vector α n}
  {ys : List.Vector β n} (f : α → β → σ × σ → (σ × σ) × γ),
  (∀ (x : α) (y : β) (s : σ),
      have s' := (f x y (s, s)).1;
      s'.1 = s'.2) →
    (List.Vector.mapAccumr₂ f xs ys (s, s)).2 =
      (List.Vector.mapAccumr₂ (fun x y s => ((f x y (s, s)).1.1, (f x y (s, s)).2)) xs ys s).2
-- Init.Data.SInt.Lemmas
Int32.toUInt32_sub : ∀ (a b : Int32), (a - b).toUInt32 = a.toUInt32 - b.toUInt32
-- Init.Data.Vector.Attach
Vector.attach_map_val : ∀ {α : Type u_1} {n : ℕ} {β : Type u_2} (xs : Vector α n) (f : α → β),
  Vector.map (fun i => f ↑i) xs.attach = Vector.map f xs
-- Mathlib.CategoryTheory.Monoidal.Types.Coyoneda
CategoryTheory.instLaxMonoidalObjOppositeFunctorTypeCoyonedaOpTensorUnit : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      (CategoryTheory.coyoneda.obj (Opposite.op (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))).LaxMonoidal
-- Lean.Elab.Declaration
/-- Update the name of the given declaration.
This function assumes `stx` is not a nameless instance.
 -/
_private.Lean.Elab.Declaration.0.Lean.Elab.Command.setDeclName : Lean.Syntax → Lean.Name → Lean.Syntax
-- Mathlib.CategoryTheory.Limits.Cones
/-- Whiskering on the left by `E : K ⥤ J` gives a functor from `Cone F` to `Cone (E ⋙ F)`.
 -/
CategoryTheory.Limits.Cone.whiskering : {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 : CategoryTheory.Functor K J) →
                CategoryTheory.Functor (CategoryTheory.Limits.Cone F) (CategoryTheory.Limits.Cone (E.comp F))
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.get?_filter : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] {f : α → Bool} {k : α},
  t.WF → (Std.TreeSet.Raw.filter f t).get? k = Option.filter f (t.get? k)
-- Batteries.Recycling.RBTree.Lemmas
/-- The value `x` returned by `lowerBound?` is less or equal to the `cut`.  -/
RBTree.RBNode.lowerBound?_le : ∀ {α : Type u_1} {cut : α → Ordering} {x : α} {t : RBTree.RBNode α},
  RBTree.RBNode.lowerBound? cut t = some x → cut x ≠ Ordering.lt
-- Mathlib.CategoryTheory.Dialectica.Monoidal
CategoryTheory.Dial.tensorObjImpl_src : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasFiniteProducts C]
  [inst_2 : CategoryTheory.Limits.HasPullbacks C] (X Y : CategoryTheory.Dial C),
  (X.tensorObjImpl Y).src = (X.src ⨯ Y.src)
-- Init.Data.Nat.Coprime
Nat.Coprime.mul_left : ∀ {m k n : ℕ}, m.Coprime k → n.Coprime k → (m * n).Coprime k
-- Mathlib.Analysis.Normed.Group.NullSubmodule
mem_nullSubmodule_iff : ∀ {𝕜 : Type u_2} {E : Type u_3} [inst : SeminormedAddCommGroup E] [inst_1 : SeminormedRing 𝕜] [inst_2 : Module 𝕜 E]
  [inst_3 : IsBoundedSMul 𝕜 E] {x : E}, x ∈ nullSubmodule 𝕜 E ↔ ‖x‖ = 0
-- Mathlib.Algebra.Group.Submonoid.Operations
AddMonoidHom.mker_inr : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N],
  AddMonoidHom.mker (AddMonoidHom.inr M N) = ⊥
-- Init.GrindInstances.Ring.SInt
Lean.Grind.Int8.natCast : NatCast Int8
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.le_maxKeyD_of_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k : α}, k ∈ t → ∀ {fallback : α}, (cmp k (t.maxKeyD fallback)).isLE = true
-- Mathlib.Analysis.Complex.Trigonometric
Real.tan_neg : ∀ (x : ℝ), Real.tan (-x) = -Real.tan x
-- Std.Data.DTreeMap.Internal.Operations
/-- Adds a new mapping to the key, overwriting an existing one with equal key if present.  -/
Std.DTreeMap.Internal.Impl.insert : {α : Type u} →
  {β : α → Type v} →
    [Ord α] →
      (k : α) →
        β k →
          (t : Std.DTreeMap.Internal.Impl α β) →
            t.Balanced → Std.DTreeMap.Internal.Impl.SizedBalancedTree α β t.size (t.size + 1)
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.singleZeroRingHom_apply : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddZeroClass M] (a : R),
  AddMonoidAlgebra.singleZeroRingHom a = (↑(AddMonoidAlgebra.singleAddHom 0)).toFun a
-- Mathlib.CategoryTheory.Functor.CurryingThree
CategoryTheory.Functor.flip₁₃_obj_obj_obj : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_4} {E : Type u_9} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_4} C₃]
  [inst_3 : CategoryTheory.Category.{v_9, u_9} E]
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ E))) (G : C₃) (H : C₂) (K : C₁),
  ((F.flip₁₃.obj G).obj H).obj K = ((F.obj K).obj H).obj G
-- Lean.Meta.Tactic.Grind.EMatch
_private.Lean.Meta.Tactic.Grind.EMatch.0.Break.runK.match_1.eq_1 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (a : α) (h_1 : (a : α) → motive (some a)) (h_2 : Unit → motive none),
  (match some a with
    | some a => h_1 a
    | none => h_2 ()) =
    h_1 a
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
mul_le_iff_le_one_left' : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : LE α] [MulRightMono α] [MulRightReflectLE α] {a b : α},
  a * b ≤ b ↔ a ≤ 1
-- Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
/-- The iterated derivative commutes with shifting the function by a constant on the left.  -/
iteratedDeriv_comp_const_add : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] (n : ℕ) (f : 𝕜 → F) (s : 𝕜),
  (iteratedDeriv n fun z => f (s + z)) = fun t => iteratedDeriv n f (s + t)
-- Mathlib.Algebra.Order.Floor.Extended
ENat.le_floor : ∀ {r : ENNReal} {n : ℕ∞}, n ≤ ⌊r⌋ₑ ↔ ↑n ≤ r