mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Calculus.FDeriv.Add
/-- If `c` is invertible, `c • f` is differentiable at `x` within `s` if and only if `f` is.  -/
differentiableWithinAt_smul_iff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {x : E} {s : Set E} {R : Type u_4} [inst_5 : Monoid R] [inst_6 : DistribMulAction R F] [SMulCommClass 𝕜 R F]
  [ContinuousConstSMul R F] (c : R) [Invertible c],
  DifferentiableWithinAt 𝕜 (c • f) s x ↔ DifferentiableWithinAt 𝕜 f s x
-- Mathlib.RingTheory.Ideal.Prod
Submodule.IsPrincipal.generator.congr_simp : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (S S_1 : Submodule R M) (e_S : S = S_1) [inst_3 : S.IsPrincipal],
  Submodule.IsPrincipal.generator S = Submodule.IsPrincipal.generator S_1
-- Mathlib.Order.LiminfLimsup
Filter.HasBasis.blimsup_eq_iInf_iSup : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : CompleteLattice α] {p : ι → Prop} {s : ι → Set β} {f : Filter β}
  {u : β → α}, f.HasBasis p s → ∀ {q : β → Prop}, Filter.blimsup u f q = ⨅ i, ⨅ (_ : p i), ⨆ a ∈ s i, ⨆ (_ : q a), u a
-- Mathlib.LinearAlgebra.RootSystem.Chain
RootPairing.chainTopCoeff_reflectionPerm_left : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Finite ι] [inst_1 : CommRing R]
  [inst_2 : CharZero R] [inst_3 : IsDomain R] [inst_4 : AddCommGroup M] [inst_5 : Module R M] [inst_6 : AddCommGroup N]
  [inst_7 : Module R N] {P : RootPairing ι R M N} [inst_8 : P.IsCrystallographic] {i j : ι},
  RootPairing.chainTopCoeff ((P.reflectionPerm i) i) j = RootPairing.chainBotCoeff i j
-- Mathlib.Topology.Constructions.SumProd
map_snd_nhds : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (x : X × Y),
  Filter.map Prod.snd (nhds x) = nhds x.2
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getElem?_inter_of_not_mem_left : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ {k : α}, k ∉ m₁ → (m₁ ∩ m₂)[k]? = none
-- Init.Data.BitVec.Basic
BitVec.cast.congr_simp : ∀ {n m : ℕ} (eq : n = m) (x x_1 : BitVec n), x = x_1 → BitVec.cast eq x = BitVec.cast eq x_1
-- Init.Data.Dyadic.Instances
Dyadic.instNoNatZeroDivisors : Lean.Grind.NoNatZeroDivisors Dyadic
-- Mathlib.Algebra.MonoidAlgebra.Module
MonoidAlgebra.smul_of : ∀ {R : Type u_1} {M : Type u_3} [inst : Semiring R] [inst_1 : MulOneClass M] (m : M) (r : R),
  r • (MonoidAlgebra.of R M) m = MonoidAlgebra.single m r
-- Init.Data.BitVec.Lemmas
BitVec.getElem_shiftConcat_zero : ∀ {w : ℕ} {x : BitVec w} (b : Bool) (h : 0 < w), (x.shiftConcat b)[0] = b
-- Mathlib.Tactic.CategoryTheory.Monoidal.Normalize
Mathlib.Tactic.Monoidal.evalHorizontalCompAux_cons : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {f f' g g' h i : C} {η : f ⟶ g} {ηs : f' ⟶ g'} {θ : h ⟶ i}
  {ηθ : CategoryTheory.MonoidalCategoryStruct.tensorObj f' h ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj g' i}
  {η₁ :
    CategoryTheory.MonoidalCategoryStruct.tensorObj f (CategoryTheory.MonoidalCategoryStruct.tensorObj f' h) ⟶
      CategoryTheory.MonoidalCategoryStruct.tensorObj g (CategoryTheory.MonoidalCategoryStruct.tensorObj g' i)}
  {ηθ₁ :
    CategoryTheory.MonoidalCategoryStruct.tensorObj f (CategoryTheory.MonoidalCategoryStruct.tensorObj f' h) ⟶
      CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj g g') i}
  {ηθ₂ :
    CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj f f') h ⟶
      CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj g g') i},
  CategoryTheory.MonoidalCategoryStruct.tensorHom ηs θ = ηθ →
    CategoryTheory.MonoidalCategoryStruct.tensorHom
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Iso.refl f).hom
            (CategoryTheory.CategoryStruct.comp η (CategoryTheory.Iso.refl g).hom))
          ηθ =
        η₁ →
      CategoryTheory.CategoryStruct.comp η₁ (CategoryTheory.MonoidalCategoryStruct.associator g g' i).inv = ηθ₁ →
        CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator f f' h).hom ηθ₁ = ηθ₂ →
          CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.tensorHom η ηs) θ = ηθ₂
-- Mathlib.Geometry.Euclidean.Altitude
/-- The definition of an altitude.  -/
Affine.Simplex.altitude_def : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P n) (i : Fin (n + 1)),
  s.altitude i =
    AffineSubspace.mk' (s.points i) (affineSpan ℝ (s.points '' {i}ᶜ)).directionᗮ ⊓ affineSpan ℝ (Set.range s.points)
-- Mathlib.Data.Set.Finite.Lattice
/-- An indexed union of pairwise disjoint sets is finite iff all sets are finite, and all but
finitely many are empty.  -/
Set.PairwiseDisjoint.finite_biUnion_iff : ∀ {α : Type u} {β : Type v} {f : β → Set α} {s : Set β},
  s.PairwiseDisjoint f → ((⋃ i ∈ s, f i).Finite ↔ (∀ i ∈ s, (f i).Finite) ∧ {i | i ∈ s ∧ (f i).Nonempty}.Finite)
-- Mathlib.MeasureTheory.Measure.HasOuterApproxClosed
/-- The integrals of thickened indicators of a closed set against a finite measure tend to the
measure of the closed set if the thickening radii tend to zero.  -/
MeasureTheory.tendsto_lintegral_thickenedIndicator_of_isClosed : ∀ {Ω : Type u_2} {mΩ : MeasurableSpace Ω} [inst : PseudoEMetricSpace Ω] [OpensMeasurableSpace Ω]
  (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] {F : Set Ω},
  IsClosed F →
    ∀ {δs : ℕ → ℝ} (δs_pos : ∀ (n : ℕ), 0 < δs n),
      Filter.Tendsto δs Filter.atTop (nhds 0) →
        Filter.Tendsto (fun n => ∫⁻ (ω : Ω), ↑((thickenedIndicator ⋯ F) ω) ∂μ) Filter.atTop (nhds (μ F))
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero
/-- A zero functor preserves limits.  -/
CategoryTheory.Functor.preservesLimitsOfShape_of_isZero : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasZeroMorphisms D] (G : CategoryTheory.Functor C D),
  CategoryTheory.Limits.IsZero G →
    ∀ (J : Type u_1) [inst_4 : CategoryTheory.Category.{v_1, u_1} J], CategoryTheory.Limits.PreservesLimitsOfShape J G
-- Mathlib.Algebra.Module.Torsion.Free
Module.isTorsionFree_iff_smul_eq_zero : ∀ {R : Type u_1} {M : Type u_3} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsDomain R],
  Module.IsTorsionFree R M ↔ ∀ (r : R) (m : M), r • m = 0 → r = 0 ∨ m = 0
-- Mathlib.RingTheory.Trace.Defs
Algebra.trace_eq_matrix_trace : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {ι : Type w}
  [inst_3 : Fintype ι] [inst_4 : DecidableEq ι] (b : Module.Basis ι R S) (s : S),
  (Algebra.trace R S) s = ((Algebra.leftMulMatrix b) s).trace
-- Mathlib.CategoryTheory.Limits.Opposites
CategoryTheory.Limits.hasLimitsOfShape_opposite_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} J],
  CategoryTheory.Limits.HasLimitsOfShape J Cᵒᵖ ↔ CategoryTheory.Limits.HasColimitsOfShape Jᵒᵖ C
-- Mathlib.Order.Hom.Basic
/-- Any type satisfying `OrderHomClass` can be cast into `OrderHom` via
`OrderHomClass.toOrderHom`.  -/
OrderHomClass.instCoeTCOrderHom : {F : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : Preorder α] → [inst_1 : Preorder β] → [inst_2 : FunLike F α β] → [OrderHomClass F α β] → CoeTC F (α →o β)
-- Mathlib.Data.Finsupp.Interval
Finsupp.card_Ico : ∀ {ι : Type u_1} {α : Type u_2} [inst : PartialOrder α] [inst_1 : Zero α] [inst_2 : LocallyFiniteOrder α]
  [inst_3 : DecidableEq ι] [inst_4 : DecidableEq α] (f g : ι →₀ α),
  (Finset.Ico f g).card = ∏ i ∈ f.support ∪ g.support, (Finset.Icc (f i) (g i)).card - 1
-- Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
Matrix.charpoly_degree_eq_dim : ∀ {R : Type u} [inst : CommRing R] {n : Type v} [inst_1 : DecidableEq n] [inst_2 : Fintype n] [Nontrivial R]
  (M : Matrix n n R), M.charpoly.degree = ↑(Fintype.card n)
-- Mathlib.Data.Int.ModEq
/-- **Alias** of the forward direction of `Int.modEq_iff_dvd`. -/
Int.ModEq.dvd : ∀ {n a b : ℤ}, a ≡ b [ZMOD n] → n ∣ b - a
-- Init.Data.Int.Basic
/-- Multiplication of integers, usually accessed via the `*` operator.

This function is overridden by the compiler with an efficient implementation. This definition is
the logical model.

Examples:
 * `(63 : Int) * (6 : Int) = 378`
 * `(6 : Int) * (-6 : Int) = -36`
 * `(7 : Int) * (0 : Int) = 0`
 -/
Int.mul : ℤ → ℤ → ℤ
-- Mathlib.AlgebraicGeometry.Geometrically.Connected
AlgebraicGeometry.instConnectedSpaceCarrierCarrierCommRingCatPullbackSchemeOfGeometricallyConnectedOfUniversallyOpen : ∀ {X Y S : AlgebraicGeometry.Scheme} (f : X ⟶ S) (g : Y ⟶ S) [AlgebraicGeometry.GeometricallyConnected f]
  [AlgebraicGeometry.UniversallyOpen f] [ConnectedSpace ↥Y], ConnectedSpace ↥(CategoryTheory.Limits.pullback f g)
-- Mathlib.Algebra.Homology.ModelCategory.Injective
CochainComplex.Plus.modelCategoryQuillen.instIsStableUnderRetractsCofibrations : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Abelian C],
  (HomotopicalAlgebra.cofibrations (CochainComplex.Plus C)).IsStableUnderRetracts
-- Mathlib.Analysis.Normed.Module.Normalize
NormedSpace.normalize_normalize : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] (x : V),
  NormedSpace.normalize (NormedSpace.normalize x) = NormedSpace.normalize x
-- Mathlib.CategoryTheory.GradedObject.Bifunctor
CategoryTheory.GradedObject.mapBifunctor_obj_map : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : 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} C₃]
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)) (I : Type u_4) (J : Type u_5)
  (X : CategoryTheory.GradedObject I C₁) {X_1 Y : CategoryTheory.GradedObject J C₂} (φ : X_1 ⟶ Y) (ij : I × J),
  ((CategoryTheory.GradedObject.mapBifunctor F I J).obj X).map φ ij = (F.obj (X ij.1)).map (φ ij.2)
-- Std.Http.Data.Headers
Std.Http.instInhabitedHeaders : Inhabited Std.Http.Headers
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometry.completeSpace_map : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} [inst_2 : SeminormedAddCommGroup E] [inst_3 : SeminormedAddCommGroup E₂] [inst_4 : Module R E]
  [inst_5 : Module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂) [inst_6 : RingHomSurjective σ₁₂] (p : Submodule R E) [CompleteSpace ↥p],
  CompleteSpace ↥(Submodule.map (↑f) p)
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
AddMonoidAlgebra.map_sum : ∀ {ι : Type u_1} {R : Type u_3} {S : Type u_4} {M : Type u_6} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+ S)
  (s : Finset ι) (x : ι → AddMonoidAlgebra R M),
  AddMonoidAlgebra.map f (∑ i ∈ s, x i) = ∑ i ∈ s, AddMonoidAlgebra.map f (x i)
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
/-- The pointwise sum of two finsets `s` and `t`: `s +ᵥ t = {x +ᵥ y | x ∈ s, y ∈ t}`.  -/
Finset.vadd : {α : Type u_2} → {β : Type u_3} → [DecidableEq β] → [VAdd α β] → VAdd (Finset α) (Finset β)
-- Mathlib.CategoryTheory.Monoidal.CommGrp_
CategoryTheory.CommGrp.mk.injEq : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X : C) [grp : CategoryTheory.GrpObj X]
  [comm : CategoryTheory.IsCommMonObj X] (X_1 : C) (grp_1 : CategoryTheory.GrpObj X_1)
  (comm_1 : CategoryTheory.IsCommMonObj X_1),
  ({ X := X, grp := grp, comm := comm } = { X := X_1, grp := grp_1, comm := comm_1 }) = (X = X_1 ∧ grp ≍ grp_1)
-- Mathlib.Topology.EMetricSpace.Defs
WeakEMetricSpace.toWeakPseudoEMetricSpace : {α : Type u} → {inst : TopologicalSpace α} → [self : WeakEMetricSpace α] → WeakPseudoEMetricSpace α
-- Lean.Server.References
/-- Removes the ilean file data at `path` from `self`.  -/
Lean.Server.References.removeIlean : Lean.Server.References → System.FilePath → Lean.Server.References
-- Mathlib.Logic.Function.Basic
Function.instReflOnFun : ∀ {α : Sort u_1} {β : Sort u_2} (r : β → β → Prop) (f : α → β) [Std.Refl r], Std.Refl (Function.onFun r f)
-- Mathlib.RingTheory.Polynomial.Basic
MvPolynomial.instFiniteOfIsEmpty : ∀ {ι : Type u_2} {R : Type u_3} [inst : CommSemiring R] [IsEmpty ι], Module.Finite R (MvPolynomial ι R)
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.equivHomsetRightOfNatIso_symm_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F F' : CategoryTheory.Functor C D} (iso : F ≅ F') {X : C} {Y : D} (g : Y ⟶ F'.obj X),
  (CategoryTheory.Adjunction.equivHomsetRightOfNatIso iso).symm g = CategoryTheory.CategoryStruct.comp g (iso.inv.app X)
-- Mathlib.GroupTheory.FiniteIndexNormalSubgroup
FiniteIndexNormalAddSubgroup.comap_mono : ∀ {G : Type u_1} [inst : AddGroup G] {H : Type u_2} [inst_1 : AddGroup H] (f : G →+ H)
  {K L : FiniteIndexNormalAddSubgroup H},
  K ≤ L → FiniteIndexNormalAddSubgroup.comap f K ≤ FiniteIndexNormalAddSubgroup.comap f L
-- Mathlib.Data.FunLike.Group
FunLike.involutiveInv.eq_1 : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : Inv F] [inst_2 : InvolutiveInv β]
  [inst_3 : IsInvApply F α β], FunLike.involutiveInv = Function.Injective.involutiveInv (fun f => ⇑f) ⋯ ⋯
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getElem_map : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp}
  [inst : Std.TransCmp cmp] [Std.LawfulEqCmp cmp] {f : α → β → γ} {k : α} {h' : k ∈ Std.TreeMap.Raw.map f t} (h : t.WF),
  (Std.TreeMap.Raw.map f t)[k] = f k t[k]
-- Mathlib.CategoryTheory.Sites.Over
CategoryTheory.GrothendieckTopology.instIsContinuousOverForgetOver : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (X : C),
  (CategoryTheory.Over.forget X).IsContinuous (J.over X) J
-- Mathlib.Analysis.Normed.Group.Seminorm
AddGroupSeminorm.comp_zero : ∀ {E : Type u_3} {F : Type u_4} [inst : AddGroup E] [inst_1 : AddGroup F] (p : AddGroupSeminorm E), p.comp 0 = 0
-- Mathlib.Analysis.Asymptotics.TVS
Asymptotics.IsLittleOTVS.trans_isThetaTVS : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} {G : Type u_6} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommGroup F]
  [inst_5 : TopologicalSpace F] [inst_6 : Module 𝕜 F] [inst_7 : AddCommGroup G] [inst_8 : TopologicalSpace G]
  [inst_9 : Module 𝕜 G] {l : Filter α} {f : α → E} {g : α → F} {k : α → G}, f =o[𝕜; l] g → g =Θ[𝕜; l] k → f =o[𝕜; l] k
-- Mathlib.RingTheory.WittVector.FrobeniusFractionField
WittVector.RecursionBase.solution_nonzero : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] {k : Type u_1} [inst : Field k] [inst_1 : IsAlgClosed k] {a₁ a₂ : WittVector p k},
  a₁.coeff 0 ≠ 0 → a₂.coeff 0 ≠ 0 → WittVector.RecursionBase.solution p a₁ a₂ ≠ 0
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Over.iteratedSliceEquivOverMapIso_hom_app_left_left : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X : T} {f g : CategoryTheory.Over X} (p : f ⟶ g)
  (X_1 : CategoryTheory.Over f),
  ((CategoryTheory.Over.iteratedSliceEquivOverMapIso p).hom.app X_1).left.left =
    CategoryTheory.CategoryStruct.id X_1.left.left
-- Mathlib.Algebra.Group.Pointwise.Set.Finite
Set.Finite.smul : ∀ {α : Type u_2} {β : Type u_3} [inst : SMul α β] {s : Set α} {t : Set β}, s.Finite → t.Finite → (s • t).Finite
-- Init.Control.Lawful.MonadAttach.Instances
StateT.map.eq_1 : ∀ {σ : Type u} {m : Type u → Type v} [inst : Monad m] {α β : Type u} (f : α → β) (x : StateT σ m α) (s : σ),
  StateT.map f x s = do
    let __x ← x s
    match __x with
      | (a, s) => pure (f a, s)
-- Lean.LibrarySuggestions.SymbolFrequency
_private.Lean.LibrarySuggestions.SymbolFrequency.0.Lean.LibrarySuggestions.symbolFrequencyExt.unsafe_impl_4 : Lean.Environment → Lean.OLeanEntries (Array (Lean.NameMap ℕ))
-- Init.Data.Int.Linear
Int.Internal.Linear.Expr.denote.eq_6 : ∀ (ctx : Int.Internal.Linear.Context) (k : ℤ) (e : Int.Internal.Linear.Expr),
  Int.Internal.Linear.Expr.denote ctx (Int.Internal.Linear.Expr.mulL k e) = k * Int.Internal.Linear.Expr.denote ctx e
-- Mathlib.Combinatorics.Colex
Finset.Colex.mem_initSeg : ∀ {α : Type u_1} [inst : LinearOrder α] {s t : Finset α} [inst_1 : Fintype α],
  t ∈ Finset.Colex.initSeg s ↔ s.card = t.card ∧ toColex t ≤ toColex s
-- Mathlib.Data.Finset.NoncommProd
/-- The non-commutative version of `Finset.sum_add_distrib`  -/
Finset.noncommSum_add_distrib : ∀ {α : Type u_3} {β : Type u_4} [inst : AddMonoid β] {s : Finset α} (f g : α → β)
  (comm_ff : (↑s).Pairwise (Function.onFun AddCommute f)) (comm_gg : (↑s).Pairwise (Function.onFun AddCommute g))
  (comm_gf : (↑s).Pairwise fun x y => AddCommute (g x) (f y)),
  s.noncommSum (f + g) ⋯ = s.noncommSum f comm_ff + s.noncommSum g comm_gg
-- Mathlib.GroupTheory.Congruence.Hom
/-- The natural homomorphism from an `AddMonoid` to its quotient by an additive
congruence relation.  -/
AddCon.mk' : {M : Type u_1} → [inst : AddZeroClass M] → (c : AddCon M) → M →+ c.Quotient
-- Mathlib.Data.ZMod.IntUnitsPower
uzpow_add : ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : Module R (Additive ℤˣ)] (s : ℤˣ) (x y : R),
  s ^ (x + y) = s ^ x * s ^ y
-- Mathlib.Analysis.Normed.Operator.NormedSpace
ContinuousLinearEquiv.coord_norm : ∀ (𝕜 : Type u_1) {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NontriviallyNormedField 𝕜]
  [inst_2 : NormedSpace 𝕜 E] (x : E) (h : x ≠ 0), ‖ContinuousLinearEquiv.coord 𝕜 x h‖ = ‖x‖⁻¹
-- Init.Data.String.Modify
String.Pos.offset_pastSet : ∀ {s : String} {p : s.Pos} {c : Char} {hp : p ≠ s.endPos}, (p.pastSet c hp).offset = p.offset + c
-- Mathlib.Algebra.Order.ToIntervalMod
/-- If `a` and `b` fall within the same cycle w.r.t. `c`, then they are congruent modulo `p`.  -/
toIcoMod_inj : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) {a b c : α}, toIcoMod hp c a = toIcoMod hp c b ↔ a ≡ b [PMOD p]
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.minKey?_insert_of_isEmpty : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k : α}
  {v : β k}, t.isEmpty = true → (t.insert k v).minKey? = some k
-- Aesop.EMap
Aesop.EMap.instForInProdExpr : {m : Type → Type u_1} → [Monad m] → {α : Type u_2} → ForIn m (Aesop.EMap α) (Lean.Expr × α)
-- Mathlib.CategoryTheory.FintypeCat
/-- The fully faithful embedding of `FintypeCat` into the category of types.  -/
FintypeCat.incl : CategoryTheory.Functor FintypeCat (Type u_1)
-- Mathlib.LinearAlgebra.Finsupp.Span
Submodule.range_lsum_smul : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} {σ : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] (φ : M →ₗ[R] N) (f : σ → R),
  ((Finsupp.lsum R) fun x => f x • φ).range = Set.range f • φ.range
-- Init.Data.String.Decode
/-- Returns the sequence of bytes in a character's UTF-8 encoding.
 -/
String.utf8EncodeCharFast : Char → List UInt8
-- Mathlib.Data.Nat.Factorial.DoubleFactorial
_private.Mathlib.Data.Nat.Factorial.DoubleFactorial.0.Nat.doubleFactorial.match_1.splitter : (motive : ℕ → Sort u_1) → (x : ℕ) → (Unit → motive 0) → (Unit → motive 1) → ((k : ℕ) → motive k.succ.succ) → motive x
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.filterMap_eq_filter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} {f : (a : α) → β a → Bool},
  Std.ExtDTreeMap.filterMap (fun k => Option.guard fun v => f k v) t = Std.ExtDTreeMap.filter f t
-- Mathlib.Order.BooleanAlgebra.Set
Set.subset_inter_union_compl_right : ∀ {α : Type u_1} (s t : Set α), s ⊆ s ∩ t ∪ tᶜ
-- Mathlib.LinearAlgebra.TensorProduct.Map
TensorProduct.map_zero_right : ∀ {R : Type u_1} {R₂ : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7}
  {N : Type u_8} {M₂ : Type u_12} {N₂ : Type u_14} [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid N]
  [inst_4 : AddCommMonoid M₂] [inst_5 : AddCommMonoid N₂] [inst_6 : Module R M] [inst_7 : Module R N]
  [inst_8 : Module R₂ M₂] [inst_9 : Module R₂ N₂] (f : M →ₛₗ[σ₁₂] M₂), TensorProduct.map f 0 = 0
-- Mathlib.Data.Finsupp.Basic
/-- **Alias** of `Finsupp.mapDomain_of_notMem_range`. -/
Finsupp.mapDomain_notin_range : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : AddCommMonoid M] {f : α → β} (x : α →₀ M),
  ∀ a ∉ Set.range f, (Finsupp.mapDomain f x) a = 0
-- Mathlib.Order.Category.Preord
Preord.instConcreteCategoryOrderHomCarrier : CategoryTheory.ConcreteCategory Preord fun x1 x2 => ↑x1 →o ↑x2
-- Mathlib.GroupTheory.FiniteIndexNormalSubgroup
FiniteIndexNormalAddSubgroup.mk.injEq : ∀ {G : Type u_1} [inst : AddGroup G] (toAddSubgroup : AddSubgroup G)
  (isNormal' : autoParam toAddSubgroup.Normal FiniteIndexNormalAddSubgroup.isNormal'._autoParam)
  (isFiniteIndex' : autoParam toAddSubgroup.FiniteIndex FiniteIndexNormalAddSubgroup.isFiniteIndex'._autoParam)
  (toAddSubgroup_1 : AddSubgroup G)
  (isNormal'_1 : autoParam toAddSubgroup_1.Normal FiniteIndexNormalAddSubgroup.isNormal'._autoParam)
  (isFiniteIndex'_1 : autoParam toAddSubgroup_1.FiniteIndex FiniteIndexNormalAddSubgroup.isFiniteIndex'._autoParam),
  ({ toAddSubgroup := toAddSubgroup, isNormal' := isNormal', isFiniteIndex' := isFiniteIndex' } =
      { toAddSubgroup := toAddSubgroup_1, isNormal' := isNormal'_1, isFiniteIndex' := isFiniteIndex'_1 }) =
    (toAddSubgroup = toAddSubgroup_1)
-- Mathlib.Algebra.Group.Indicator
map_indicator : ∀ {α : Type u_1} {M : Type u_6} {N : Type u_7} {F : Type u_8} [inst : Zero M] [inst_1 : Zero N] [inst_2 : FunLike F M N]
  [ZeroHomClass F M N] (f : F) (s : Set α) (g : α → M) (x : α), f (s.indicator g x) = s.indicator (⇑f ∘ g) x
-- Mathlib.Algebra.GroupWithZero.Basic
/-- To match `one_mul_eq_id`.  -/
zero_mul_eq_const : ∀ {M₀ : Type u_1} [inst : MulZeroClass M₀], (fun x => 0 * x) = Function.const M₀ 0
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarAlgebra.coe_iInf : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : NonUnitalSemiring A]
  [inst_3 : StarRing A] [inst_4 : Module R A] [inst_5 : IsScalarTower R A A] [inst_6 : SMulCommClass R A A]
  [inst_7 : StarModule R A] {ι : Sort u_1} {S : ι → NonUnitalStarSubalgebra R A}, ↑(⨅ i, S i) = ⋂ i, ↑(S i)
-- Mathlib.ModelTheory.Equivalence
FirstOrder.Language.BoundedFormula.imp_iff_not_sup : ∀ {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {n : ℕ} (φ ψ : L.BoundedFormula α n),
  T.Iff (φ.imp ψ) (φ.not ⊔ ψ)
-- Mathlib.Algebra.Order.Floor.Ring
Int.floor_intCast_add : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] [IsOrderedRing R] (z : ℤ) (a : R),
  ⌊↑z + a⌋ = z + ⌊a⌋
-- Init.Data.List.Perm
List.Perm.erase : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] (a : α) {l₁ l₂ : List α}, l₁.Perm l₂ → (l₁.erase a).Perm (l₂.erase a)
-- Mathlib.Topology.Closure
frontier_eq_inter_compl_interior : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, frontier s = (interior s)ᶜ ∩ (interior sᶜ)ᶜ
-- Batteries.Data.List.Lemmas
List.disjoint_take_drop : ∀ {α : Type u_1} {m n : ℕ} {l : List α}, l.Nodup → m ≤ n → (List.take m l).Disjoint (List.drop n l)
-- Mathlib.Data.ZMod.Basic
/-- So-named because the outer coercion is `Int.cast` into `ZMod`. For `Int.cast` into an arbitrary
ring, see `ZMod.intCast_cast`.  -/
ZMod.intCast_zmod_cast : ∀ {n : ℕ} (a : ZMod n), ↑a.cast = a
-- Init.Grind.Module.Envelope
Lean.Grind.IntModule.OfNatModule.instAssociativeHAdd : ∀ (α : Type u) [inst : Lean.Grind.NatModule α], Std.Associative fun x1 x2 => x1 + x2