mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
EisensteinSeries.G2_eq_tsum_cexp : ∀ (z : UpperHalfPlane),
  EisensteinSeries.G2 z =
    2 * riemannZeta 2 -
      8 * ↑Real.pi ^ 2 *
        ∑' (n : ℕ+), ↑((ArithmeticFunction.sigma 1) ↑n) * Complex.exp (2 * ↑Real.pi * Complex.I * ↑z) ^ ↑n
-- Mathlib.Topology.Algebra.Group.Basic
Filter.map_mul_left_nhdsNE : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Group G] [SeparatelyContinuousMul G] {c a : G},
  Filter.map (fun x => c * x) (nhdsWithin a {a}ᶜ) = nhdsWithin (c * a) {c * a}ᶜ
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
NumberField.mixedEmbedding.fundamentalCone.idealSet.eq_1 : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K]
  (J : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))),
  NumberField.mixedEmbedding.fundamentalCone.idealSet K J =
    NumberField.mixedEmbedding.fundamentalCone K ∩
      ↑(NumberField.mixedEmbedding.idealLattice K ((FractionalIdeal.mk0 K) J))
-- Mathlib.LinearAlgebra.LinearIndependent.Lemmas
/-- A finite family of vectors `v i` is linear independent iff the linear map that sends
`c : ι → R` to `∑ i, c i • v i` has the trivial kernel.  -/
Fintype.linearIndependent_iff' : ∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [inst : Ring R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : Fintype ι] [inst_4 : DecidableEq ι],
  LinearIndependent R v ↔ ((LinearMap.lsum R (fun x => R) ℕ) fun i => LinearMap.id.smulRight (v i)).ker = ⊥
-- Mathlib.Combinatorics.SimpleGraph.Basic
/-- The difference of two graphs `x \ y` has the edges of `x` with the edges of `y` removed.  -/
SimpleGraph.sdiff : {V : Type u} → SDiff (SimpleGraph V)
-- Init.Data.Nat.Div.Basic
Nat.mul_div_le : ∀ (m n : ℕ), n * (m / n) ≤ m
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.adjoin.range_algebraMap_subset : ∀ (F : Type u_1) [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] (S : Set E),
  Set.range ⇑(algebraMap F E) ⊆ ↑(IntermediateField.adjoin F S)
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.forget₂_moduleCat_map : ∀ {k : Type u} {G : Type v} [inst : Ring k] [inst_1 : Monoid G] {A B : Rep.{w, u, v} k G} (f : A ⟶ B),
  (CategoryTheory.forget₂ (Rep.{w, u, v} k G) (ModuleCat k)).map f = ModuleCat.ofHom (Rep.Hom.hom f).toLinearMap
-- Mathlib.Data.List.Defs
/-- `extractp p l` returns a pair of an element `a` of `l` satisfying the predicate
`p`, and `l`, with `a` removed. If there is no such element `a` it returns `(none, l)`.  -/
List.extractp : {α : Type u_1} → (p : α → Prop) → [DecidablePred p] → List α → Option α × List α
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Expr.toPolyC.go.match_4.congr_eq_9 : ∀ (motive : Lean.Grind.CommRing.Expr → Sort u_1) (x : Lean.Grind.CommRing.Expr)
  (h_1 : (k : ℤ) → motive (Lean.Grind.CommRing.Expr.num k))
  (h_2 : (k : ℕ) → motive (Lean.Grind.CommRing.Expr.natCast k))
  (h_3 : (k : ℤ) → motive (Lean.Grind.CommRing.Expr.intCast k))
  (h_4 : (x : Lean.Grind.CommRing.Var) → motive (Lean.Grind.CommRing.Expr.var x))
  (h_5 : (a b : Lean.Grind.CommRing.Expr) → motive (a.add b))
  (h_6 : (a b : Lean.Grind.CommRing.Expr) → motive (a.mul b)) (h_7 : (a : Lean.Grind.CommRing.Expr) → motive a.neg)
  (h_8 : (a b : Lean.Grind.CommRing.Expr) → motive (a.sub b))
  (h_9 : (a : Lean.Grind.CommRing.Expr) → (k : ℕ) → motive (a.pow k)) (a : Lean.Grind.CommRing.Expr) (k : ℕ),
  x = a.pow k →
    (match x with
      | Lean.Grind.CommRing.Expr.num k => h_1 k
      | Lean.Grind.CommRing.Expr.natCast k => h_2 k
      | Lean.Grind.CommRing.Expr.intCast k => h_3 k
      | Lean.Grind.CommRing.Expr.var x => h_4 x
      | a.add b => h_5 a b
      | a.mul b => h_6 a b
      | a.neg => h_7 a
      | a.sub b => h_8 a b
      | a.pow k => h_9 a k) ≍
      h_9 a k
-- Mathlib.Algebra.Homology.DerivedCategory.KProjective
CochainComplex.IsKProjective.Qh_map_bijective : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] (K : CochainComplex C ℤ) (L : HomotopyCategory C (ComplexShape.up ℤ))
  [K.IsKProjective], Function.Bijective DerivedCategory.Qh.map
-- Mathlib.CategoryTheory.Linear.Basic
/-- compatibility of the scalar multiplication with the pre-composition  -/
CategoryTheory.Linear.comp_smul : ∀ {R : Type w} {inst : Semiring R} {C : Type u} {inst_1 : CategoryTheory.Category.{v, u} C}
  {inst_2 : CategoryTheory.Preadditive C} [self : CategoryTheory.Linear R C] (X Y Z : C) (f : X ⟶ Y) (r : R)
  (g : Y ⟶ Z), CategoryTheory.CategoryStruct.comp f (r • g) = r • CategoryTheory.CategoryStruct.comp f g
-- Mathlib.CategoryTheory.Sites.IsSheafFor
CategoryTheory.Presieve.FamilyOfElements.sieveExtend.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C}
  {R : CategoryTheory.Presieve X} (x : CategoryTheory.Presieve.FamilyOfElements P R) (x_1 : C) (x_2 : x_1 ⟶ X)
  (hf : (CategoryTheory.Sieve.generate R).arrows x_2),
  x.sieveExtend x_2 hf = (CategoryTheory.ConcreteCategory.hom (P.map ⋯.choose.op)) (x ⋯.choose ⋯)
-- Mathlib.Algebra.Group.Equiv.Opposite
MulEquiv.opOp_apply : ∀ (M : Type u_3) [inst : Mul M] (a : M), (MulEquiv.opOp M) a = MulOpposite.op (MulOpposite.op a)
-- Init.Data.Function
Function.curry_uncurry : ∀ {α : Type u_1} {β : Type u_2} {φ : Sort u_3} (f : α → β → φ), Function.curry (Function.uncurry f) = f
-- Mathlib.Topology.Covering.Quotient
IsQuotientCoveringMap.homeomorph_comp_iff : ∀ {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] {Y : Type u_4} [inst_4 : TopologicalSpace Y] (φ : X ≃ₜ Y),
  IsQuotientCoveringMap (⇑φ ∘ f) G ↔ IsQuotientCoveringMap f G
-- Aesop.Index.Forward
/-- Trace the rules contained in `idx` if `traceOpt` is enabled.  -/
Aesop.ForwardIndex.trace : Aesop.TraceOption → Aesop.ForwardIndex → Lean.CoreM Unit
-- Lean.Meta.Tactic.Simp.Arith.Nat.Basic
Lean.Meta.Simp.Arith.Nat.instReprPolyCnstr_lean.repr : Nat.Internal.Linear.PolyCnstr → ℕ → Std.Format
-- Mathlib.Order.PrimeIdeal
Order.Ideal.IsPrime.mem_or_mem : ∀ {P : Type u_1} [inst : SemilatticeInf P] {I : Order.Ideal P}, I.IsPrime → ∀ {x y : P}, x ⊓ y ∈ I → x ∈ I ∨ y ∈ I
-- Mathlib.MeasureTheory.SetSemiring
MeasureTheory.IsSetSemiring.sUnion_insert_disjointOfDiff : ∀ {α : Type u_1} {C : Set (Set α)} {s t : Set α} (hC : MeasureTheory.IsSetSemiring C) (hs : s ∈ C) (ht : t ∈ C),
  t ⊆ s → ⋃₀ insert t ↑(hC.disjointOfDiff hs ht) = s
-- Mathlib.CategoryTheory.Adjunction.Opposites
CategoryTheory.Functor.IsRightAdjoint.leftOp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C Dᵒᵖ} [F.IsRightAdjoint], F.leftOp.IsLeftAdjoint
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.smulCommClass : ∀ {R : Type u_1} {M : Type u_4} {N : Type u_5} {O : Type u_6} [inst : Semiring R] [inst_1 : SMulZeroClass N R]
  [inst_2 : SMulZeroClass O R] [SMulCommClass N O R], SMulCommClass N O (MonoidAlgebra R M)
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.not_mem_inter_of_not_mem_left : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [Std.TransCmp cmp] {k : α}, k ∉ t₁ → k ∉ t₁ ∩ t₂
-- Mathlib.Tactic.Order.CollectFacts
Mathlib.Tactic.Order.AtomicFact.isInf.inj : ∀ {lhs rhs res lhs_1 rhs_1 res_1 : ℕ},
  Mathlib.Tactic.Order.AtomicFact.isInf lhs rhs res = Mathlib.Tactic.Order.AtomicFact.isInf lhs_1 rhs_1 res_1 →
    lhs = lhs_1 ∧ rhs = rhs_1 ∧ res = res_1
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.contains_insert! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF →
    ∀ {k a : α} {v : β k},
      Std.DTreeMap.Internal.Impl.contains a (Std.DTreeMap.Internal.Impl.insert! k v t) =
        (compare k a == Ordering.eq || Std.DTreeMap.Internal.Impl.contains a t)
-- Mathlib.NumberTheory.FLT.Polynomial
fermatLastTheoremWith'_polynomial : ∀ {k : Type u_1} [inst : Field k] {n : ℕ}, 3 ≤ n → ↑n ≠ 0 → FermatLastTheoremWith' (Polynomial k) n
-- Mathlib.AlgebraicGeometry.Geometrically.Connected
AlgebraicGeometry.GeometricallyConnected.connectedSpace : ∀ {X S : AlgebraicGeometry.Scheme} (f : X ⟶ S) [AlgebraicGeometry.GeometricallyConnected f] [ConnectedSpace ↥S],
  IsOpenMap ⇑f → ConnectedSpace ↥X
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.diseq_split : ∀ {α : Type u_1} [inst : Lean.Grind.IntModule α] [inst_1 : LE α] [inst_2 : LT α] [Std.LawfulOrderLT α]
  [inst_4 : Std.IsLinearOrder α] [Lean.Grind.OrderedAdd α] (ctx : Lean.Grind.Linarith.Context α)
  (p₁ p₂ : Lean.Grind.Linarith.Poly),
  Lean.Grind.Linarith.diseq_split_cert p₁ p₂ = true →
    Lean.Grind.Linarith.Poly.denote' ctx p₁ ≠ 0 →
      Lean.Grind.Linarith.Poly.denote' ctx p₁ < 0 ∨ Lean.Grind.Linarith.Poly.denote' ctx p₂ < 0
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Ioc_union_Ioi_eq_Ioi : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, a ≤ b → Set.Ioc a b ∪ Set.Ioi b = Set.Ioi a
-- Mathlib.Geometry.Euclidean.PerpBisector
/-- If `p` lies on the perpendicular bisector of `ab` and `b` is weakly between `a` and `c`,
then `p` is at least as close to `b` as to `c`.  -/
EuclideanGeometry.dist_le_of_wbtw_of_mem_perpBisector : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {a b c p : P},
  Wbtw ℝ a b c → a ≠ b → p ∈ AffineSubspace.perpBisector a b → dist p b ≤ dist p c
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.mapComp_assoc_right_inv_app_assoc : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat)
  {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (X : ↑(F.obj a)) {Z : ↑(F.obj d)}
  (h_1 : (F.map (CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h))).toFunctor.obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((F.mapComp g h).inv.toNatTrans.app ((F.map f).toFunctor.obj X))
      (CategoryTheory.CategoryStruct.comp ((F.mapComp f (CategoryTheory.CategoryStruct.comp g h)).inv.toNatTrans.app X)
        h_1) =
    CategoryTheory.CategoryStruct.comp ((F.map h).toFunctor.map ((F.mapComp f g).inv.toNatTrans.app X))
      (CategoryTheory.CategoryStruct.comp ((F.mapComp (CategoryTheory.CategoryStruct.comp f g) h).inv.toNatTrans.app X)
        (CategoryTheory.CategoryStruct.comp ((F.map₂ (CategoryTheory.Bicategory.associator f g h).hom).toNatTrans.app X)
          h_1))
-- Mathlib.Algebra.Order.Hom.Monoid
strictAnti_iff_map_neg : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α]
  [inst_3 : AddCommGroup β] [inst_4 : PartialOrder β] [IsOrderedAddMonoid β] [i : FunLike F α β] (f : F)
  [iamhc : AddMonoidHomClass F α β], StrictAnti ⇑f ↔ ∀ (a : α), 0 < a → f a < 0
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
instConditionallyCompleteLinearOrderBotWithBotOfConditionallyCompleteLinearOrder : {α : Type u_1} → [ConditionallyCompleteLinearOrder α] → ConditionallyCompleteLinearOrderBot (WithBot α)
-- Lean.Data.PersistentArray
Lean.PersistentArray.mkNewPath : {α : Type u} → USize → Array α → Lean.PersistentArrayNode α
-- Mathlib.AlgebraicTopology.ExtraDegeneracy
/-- The shift of a morphism `f : ⦋n⦌ → Δ` in `SimplexCategory` corresponds to
the monotone map which sends `0` to `0` and `i.succ` to `f.toOrderHom i`.  -/
SSet.Augmented.StandardSimplex.shift : {n : ℕ} → {Δ : SimplexCategory} → ({ len := n } ⟶ Δ) → ({ len := n + 1 } ⟶ Δ)
-- Mathlib.Algebra.MonoidAlgebra.Basic
AddMonoidAlgebra.algebraAddMonoidAlgebra.eq_1 : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_7} [inst : AddCommMonoid M] [inst_1 : CommSemiring R]
  [inst_2 : CommSemiring S] [inst_3 : Algebra R S],
  AddMonoidAlgebra.algebraAddMonoidAlgebra = (AddMonoidAlgebra.mapRingHom M (algebraMap R S)).toAlgebra
-- Mathlib.CategoryTheory.Enriched.FunctorCategory
/-- The composition for the `V`-enrichment of the category `J ⥤ C`.  -/
CategoryTheory.Enriched.FunctorCategory.enrichedComp : (V : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} V] →
    [inst_1 : CategoryTheory.MonoidalCategory V] →
      {C : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} C] →
          {J : Type u₃} →
            [inst_3 : CategoryTheory.Category.{v₃, u₃} J] →
              [inst_4 : CategoryTheory.EnrichedOrdinaryCategory V C] →
                (F₁ F₂ F₃ : CategoryTheory.Functor J C) →
                  [inst_5 : CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom V F₁ F₂] →
                    [inst_6 : CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom V F₂ F₃] →
                      [inst_7 : CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom V F₁ F₃] →
                        CategoryTheory.MonoidalCategoryStruct.tensorObj
                            (CategoryTheory.Enriched.FunctorCategory.enrichedHom V F₁ F₂)
                            (CategoryTheory.Enriched.FunctorCategory.enrichedHom V F₂ F₃) ⟶
                          CategoryTheory.Enriched.FunctorCategory.enrichedHom V F₁ F₃
-- Mathlib.Topology.Algebra.LinearTopology
IsLinearTopology.hasBasis_submodule' : ∀ {R : Type u_1} {M : Type u_3} {inst : Ring R} {inst_1 : AddCommGroup M} {inst_2 : Module R M}
  {inst_3 : TopologicalSpace M} [self : IsLinearTopology R M], (nhds 0).HasBasis (fun N => ↑N ∈ nhds 0) fun N => ↑N
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.Struct.commInst? : Lean.Meta.Grind.AC.Struct → Option Lean.Expr
-- Mathlib.Algebra.Group.Defs
AddCommGroup.mk : {G : Type u} → [toAddGroup : AddGroup G] → (∀ (a b : G), a + b = b + a) → AddCommGroup G
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.Monoidal.commTensorLeft_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.Monoidal] (X X_1 : C),
  (CategoryTheory.Functor.Monoidal.commTensorLeft F X).hom.app X_1 = CategoryTheory.Functor.LaxMonoidal.μ F X X_1
-- Init.Data.String.Lemmas.Pattern.Split.Pred
String.Slice.toList_split_bool : ∀ {s : String.Slice} {p : Char → Bool},
  List.map String.Slice.copy (s.split p).toList = List.map String.ofList (List.splitOnP p s.copy.toList)
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.get!_empty : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : Inhabited α] {a : α}, ∅.get! a = default
-- Init.Data.String.Lemmas.Pattern.Pred
String.Slice.contains_prop_eq_contains_decide : ∀ {p : Char → Prop} [inst : DecidablePred p] {s : String.Slice}, s.contains p = s.contains fun x => decide (p x)
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Path.Homotopy.transAssocReparamAux_one : Path.Homotopy.transAssocReparamAux 1 = 1
-- Mathlib.Algebra.Category.Grp.ZModuleEquivalence
/-- The forgetful functor from `ℤ` modules to `AddCommGrpCat` is full.  -/
ModuleCat.forget₂_addCommGroup_full : (CategoryTheory.forget₂ (ModuleCat ℤ) AddCommGrpCat).Full
-- Mathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy
CategoryTheory.Arrow.LeftHomotopy.ext_iff : ∀ {V : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} V} {inst_1 : CategoryTheory.Preadditive V}
  {u v : CategoryTheory.Arrow V} {f g : u ⟶ v} {x y : CategoryTheory.Arrow.LeftHomotopy f g}, x = y ↔ x.hom = y.hom
-- Mathlib.Algebra.Category.MonCat.Basic
AddCommMonCat.hom_comp : ∀ {M N T : AddCommMonCat} (f : M ⟶ N) (g : N ⟶ T),
  AddCommMonCat.Hom.hom (CategoryTheory.CategoryStruct.comp f g) =
    (AddCommMonCat.Hom.hom g).comp (AddCommMonCat.Hom.hom f)
-- Mathlib.Data.ENNReal.Basic
ENNReal.top_ne_ofReal : ∀ {r : ℝ}, ⊤ ≠ ENNReal.ofReal r
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.IsFundamentalDomain.measure_fundamentalFrontier : ∀ {G : Type u_1} {α : Type u_3} [Countable G] [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α]
  {μ : MeasureTheory.Measure α} {s : Set α},
  MeasureTheory.IsFundamentalDomain G s μ → μ (MeasureTheory.fundamentalFrontier G s) = 0
-- Mathlib.LinearAlgebra.AffineSpace.Slope
StrictAntiOn.slope_neg : ∀ {k : Type u_1} {E : Type u_2} [inst : Field k] [inst_1 : AddCommGroup E] [inst_2 : Module k E]
  [inst_3 : LinearOrder k] [IsStrictOrderedRing k] [inst_5 : PartialOrder E] [IsOrderedAddMonoid E] [PosSMulMono k E]
  {f : k → E} {x y : k} {s : Set k}, StrictAntiOn f s → x ∈ s → y ∈ s → x ≠ y → slope f x y < 0
-- Init.Data.Int.Linear
Int.Internal.Linear.Expr.mulL.inj : ∀ {k : ℤ} {a : Int.Internal.Linear.Expr} {k_1 : ℤ} {a_1 : Int.Internal.Linear.Expr},
  Int.Internal.Linear.Expr.mulL k a = Int.Internal.Linear.Expr.mulL k_1 a_1 → k = k_1 ∧ a = a_1
-- Mathlib.RepresentationTheory.Invariants
Representation.isProj_averageMap : ∀ {k : Type u_1} {G : Type u_2} {V : Type u_3} [inst : CommRing k] [inst_1 : Group G] [inst_2 : AddCommGroup V]
  [inst_3 : Module k V] (ρ : Representation k G V) [inst_4 : Fintype G] [inst_5 : Invertible ↑(Fintype.card G)],
  LinearMap.IsProj ρ.invariants ρ.averageMap
-- Mathlib.Analysis.Analytic.Composition
/-- Target set in the change of variables to compute the composition of partial sums of formal
power series, here given a a finset.
See also `comp_partialSum`.  -/
FormalMultilinearSeries.compPartialSumTarget : ℕ → ℕ → ℕ → Finset ((n : ℕ) × Composition n)
-- Mathlib.Analysis.Analytic.Basic
hasFPowerSeriesWithinOnBall_univ : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal},
  HasFPowerSeriesWithinOnBall f p Set.univ x r ↔ HasFPowerSeriesOnBall f p x r
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
SemiNormedGrp.Hom.addCommGroup : {V W : SemiNormedGrp} → AddCommGroup (V ⟶ W)
-- Mathlib.Analysis.Calculus.FDeriv.Comp
HasFDerivWithinAt.comp_hasFDerivAt : ∀ {𝕜 : 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] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f : E → F} {f' : E →L[𝕜] F} (x : E) {g : F → G}
  {g' : F →L[𝕜] G} {t : Set F},
  HasFDerivWithinAt g g' t (f x) →
    HasFDerivAt f f' x → (∀ᶠ (x' : E) in nhds x, f x' ∈ t) → HasFDerivAt (g ∘ f) (g' ∘SL f') x
-- Init.Data.Int.DivMod.Lemmas
Int.mul_tdiv_mul_of_pos : ∀ {a : ℤ} (b c : ℤ), 0 < a → (a * b).tdiv (a * c) = b.tdiv c
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd
SSet.prodStdSimplex.instIsInnerPairingCoreSucc : ∀ {m : ℕ} (k : Fin m) (n : ℕ), (SSet.prodStdSimplex.pairingCore k.succ n).IsInner
-- Mathlib.Combinatorics.SimpleGraph.Copy
SimpleGraph.copyCount_eq_zero : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} [inst : Fintype V], G.copyCount H = 0 ↔ H.Free G
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.Poly.combine.match_1.congr_eq_3 : ∀ (motive : Lean.Grind.Linarith.Poly → Lean.Grind.Linarith.Poly → Sort u_1) (p₁ p₂ : Lean.Grind.Linarith.Poly)
  (h_1 : (p₂ : Lean.Grind.Linarith.Poly) → motive Lean.Grind.Linarith.Poly.nil p₂)
  (h_2 : (p₁ : Lean.Grind.Linarith.Poly) → motive p₁ Lean.Grind.Linarith.Poly.nil)
  (h_3 :
    (a₁ : ℤ) →
      (x₁ : Lean.Grind.Linarith.Var) →
        (p₁ : Lean.Grind.Linarith.Poly) →
          (a₂ : ℤ) →
            (x₂ : Lean.Grind.Linarith.Var) →
              (p₂ : Lean.Grind.Linarith.Poly) →
                motive (Lean.Grind.Linarith.Poly.add a₁ x₁ p₁) (Lean.Grind.Linarith.Poly.add a₂ x₂ p₂))
  (a₁ : ℤ) (x₁ : Lean.Grind.Linarith.Var) (p₁_1 : Lean.Grind.Linarith.Poly) (a₂ : ℤ) (x₂ : Lean.Grind.Linarith.Var)
  (p₂_1 : Lean.Grind.Linarith.Poly),
  p₁ = Lean.Grind.Linarith.Poly.add a₁ x₁ p₁_1 →
    p₂ = Lean.Grind.Linarith.Poly.add a₂ x₂ p₂_1 →
      (match p₁, p₂ with
        | Lean.Grind.Linarith.Poly.nil, p₂ => h_1 p₂
        | p₁, Lean.Grind.Linarith.Poly.nil => h_2 p₁
        | Lean.Grind.Linarith.Poly.add a₁ x₁ p₁, Lean.Grind.Linarith.Poly.add a₂ x₂ p₂ => h_3 a₁ x₁ p₁ a₂ x₂ p₂) ≍
        h_3 a₁ x₁ p₁_1 a₂ x₂ p₂_1
-- Mathlib.MeasureTheory.Measure.Stieltjes
Ioo_subset_Iotop : ∀ {R : Type u_1} [inst : LinearOrder R] {a b : R}, Set.Ioo a b ⊆ Iotop a b
-- Mathlib.Algebra.Group.Submonoid.Units
/-- The equivalence between the additive subgroup of additive units of
`S` and the additive submonoid of additive unit elements of `S`.  -/
AddSubmonoid.addUnitsEquivIsAddUnitAddSubmonoid : {M : Type u_1} → [inst : AddMonoid M] → (S : AddSubmonoid M) → ↥S.addUnits ≃+ ↥(IsAddUnit.addSubmonoid ↥S)
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.aut_mul : ∀ {R : Type uR} {A₁ : Type uA₁} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Algebra R A₁]
  (ϕ ψ : A₁ ≃ₐ[R] A₁), ϕ * ψ = ψ.trans ϕ
-- Mathlib.MeasureTheory.Measure.TightNormed
MeasureTheory.tendsto_measure_compl_closedBall_of_isTightMeasureSet : ∀ {E : Type u_1} {mE : MeasurableSpace E} {S : Set (MeasureTheory.Measure E)} [inst : PseudoMetricSpace E],
  MeasureTheory.IsTightMeasureSet S →
    ∀ (x : E), Filter.Tendsto (fun r => ⨆ μ ∈ S, μ (Metric.closedBall x r)ᶜ) Filter.atTop (nhds 0)
-- Mathlib.CategoryTheory.Subobject.Limits
CategoryTheory.Limits.kernelSubobjectMap_arrow_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {f : X ⟶ Y} [inst_2 : CategoryTheory.Limits.HasKernel f] {X' Y' : C} {f' : X' ⟶ Y'}
  [inst_3 : CategoryTheory.Limits.HasKernel f'] (sq : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk f')
  {F : C → C → Type uF} {carrier : C → Type w} {instFunLike : (X Y : C) → FunLike (F X Y) (carrier X) (carrier Y)}
  [inst_4 : CategoryTheory.ConcreteCategory C F]
  (x : carrier (CategoryTheory.Subobject.underlying.obj (CategoryTheory.Limits.kernelSubobject f))),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.kernelSubobject f').arrow)
      ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.kernelSubobjectMap sq)) x) =
    (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Arrow.Hom.left sq))
      ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.kernelSubobject f).arrow) x)
-- Mathlib.Algebra.Torsor.Defs
/-- The permutation given by `p ↦ v +ᵥ p`.  -/
Equiv.constVAdd : {G : Type u_1} → (P : Type u_2) → [inst : AddGroup G] → [AddTorsor G P] → G → Equiv.Perm P
-- Mathlib.Algebra.Order.Sub.Unbundled.Basic
AddLECancellable.add_tsub_assoc_of_le : ∀ {α : Type u_1} [inst : AddCommSemigroup α] [inst_1 : PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α]
  [inst_4 : Sub α] [OrderedSub α] {b c : α}, AddLECancellable c → c ≤ b → ∀ (a : α), a + b - c = a + (b - c)
-- Mathlib.Order.CompleteLattice.Basic
iSup_dite : ∀ {α : Type u_1} {ι : Sort u_4} [inst : CompleteLattice α] (p : ι → Prop) [inst_1 : DecidablePred p]
  (f : (i : ι) → p i → α) (g : (i : ι) → ¬p i → α),
  (⨆ i, if h : p i then f i h else g i h) = (⨆ i, ⨆ (h : p i), f i h) ⊔ ⨆ i, ⨆ (h : ¬p i), g i h
-- Mathlib.Order.Disjoint
codisjoint_right_comm : ∀ {α : Type u_1} [inst : SemilatticeSup α] [inst_1 : OrderTop α] {a b c : α},
  Codisjoint (a ⊔ b) c ↔ Codisjoint (a ⊔ c) b
-- Mathlib.AlgebraicGeometry.Gluing
/-- An equivalence relation on `Σ i, D.U i` that holds iff `𝖣.ι i x = 𝖣.ι j y`.
See `AlgebraicGeometry.Scheme.GlueData.ι_eq_iff`.  -/
AlgebraicGeometry.Scheme.GlueData.Rel : (D : AlgebraicGeometry.Scheme.GlueData) → (i : D.J) × ↥(D.U i) → (i : D.J) × ↥(D.U i) → Prop
-- Mathlib.SetTheory.Cardinal.ENat
Cardinal.toENatAux_nat : ∀ (n : ℕ), (↑n).toENatAux = ↑n
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
Filter.EventuallyEq.mfderiv_eq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f f₁ : M → M'} {x : M},
  f₁ =ᶠ[nhds x] f → mfderiv% f₁ x = mfderiv% f x