mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Category.Ring.FilteredColimits
SemiRingCat.FilteredColimits.colimitSemiring : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    (F : CategoryTheory.Functor J SemiRingCat) →
      [inst_1 : CategoryTheory.IsFiltered J] → Semiring ↑(SemiRingCat.FilteredColimits.R F)
-- Mathlib.CategoryTheory.Monad.Products
CategoryTheory.coprodMonad_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : C) [inst_1 : CategoryTheory.Limits.HasBinaryCoproducts C]
  (Y : C), (CategoryTheory.coprodMonad X).obj Y = (X ⨿ Y)
-- Mathlib.RepresentationTheory.Homological.Resolution
/-- Given a `k`-linear `G`-representation `V`, `Extⁿ(k, V)` (where `k` is the trivial `k`-linear
`G`-representation) is isomorphic to the `n`th cohomology group of `Hom(P, V)`, where `P` is the
bar resolution of `k`.  -/
Rep.barResolution.extIso : (k G : Type u) →
  [inst : CommRing k] →
    [inst_1 : Group G] →
      (V : Rep.{u, u, u} k G) →
        (n : ℕ) →
          ((Ext k (Rep.{u, u, u} k G) n).obj (Opposite.op (Rep.trivial k G k))).obj V ≅
            HomologicalComplex.homology ((Rep.barComplex k G).linearYonedaObj k V) n
-- Init.Core
DoResultBC.break.injEq : ∀ {σ : Type u} (a a_1 : σ), (DoResultBC.break a = DoResultBC.break a_1) = (a = a_1)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
WeierstrassCurve.Affine.derivative_addPolynomial_slope : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Affine F} [inst_1 : DecidableEq F] {x₁ x₂ y₁ y₂ : F},
  W.Equation x₁ y₁ →
    W.Equation x₂ y₂ →
      ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂) →
        Polynomial.derivative (W.addPolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)) =
          -((Polynomial.X - Polynomial.C x₁) * (Polynomial.X - Polynomial.C x₂) +
                (Polynomial.X - Polynomial.C x₁) * (Polynomial.X - Polynomial.C (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))) +
              (Polynomial.X - Polynomial.C x₂) * (Polynomial.X - Polynomial.C (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))))
-- Mathlib.LinearAlgebra.Multilinear.DFinsupp
MultilinearMap.freeDFinsuppEquiv_def : ∀ {ι : Type uι} {κ : ι → Type uκ} {R : Type uR} {ι' : Type u_1} [inst : DecidableEq ι] [inst_1 : Fintype ι]
  [inst_2 : CommSemiring R] [inst_3 : (i : ι) → Fintype (κ i)] [inst_4 : (i : ι) → DecidableEq (κ i)]
  (f : Π₀ (x : ((i : ι) → κ i) × ι'), R),
  MultilinearMap.freeDFinsuppEquiv f =
    (MultilinearMap.fromDFinsuppEquiv κ R)
      ((LinearEquiv.piCongrRight fun x => MultilinearMap.piRingEquiv)
        (DFinsupp.linearEquivFunOnFintype
          (DFinsupp.sigmaCurryLEquiv ((DFinsupp.domLCongr (Equiv.sigmaEquivProd ((i : ι) → κ i) ι').symm) f))))
-- Mathlib.RingTheory.Derivation.MapCoeffs
Differential.mapCoeffs_X : ∀ {A : Type u_1} [inst : CommRing A] [inst_1 : Differential A], Differential.mapCoeffs Polynomial.X = 0
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.isUnit_dblZ_of_Y_ne' : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Jacobian F} {P Q : Fin 3 → F},
  W.Equation P →
    W.Equation Q → P 2 ≠ 0 → P 0 * Q 2 ^ 2 = Q 0 * P 2 ^ 2 → P 1 * Q 2 ^ 3 ≠ W.negY Q * P 2 ^ 3 → IsUnit (W.dblZ P)
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology
/-- `CohomologyClass K L m` identifies to the cohomology of the complex `HomComplex K L`
in degree `m`.  -/
CochainComplex.HomComplex.leftHomologyData' : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      (K L : CochainComplex C ℤ) →
        (n m p : ℤ) → n + 1 = m → m + 1 = p → (HomologicalComplex.sc' (K.HomComplex L) n m p).LeftHomologyData
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.LetValue.isShared.inj : ∀ {pu : Lean.Compiler.LCNF.Purity} {fvarId : Lean.FVarId}
  {h : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.LetValue._auto_25} {fvarId_1 : Lean.FVarId}
  {h_1 : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.LetValue._auto_25},
  Lean.Compiler.LCNF.LetValue.isShared fvarId h = Lean.Compiler.LCNF.LetValue.isShared fvarId_1 h_1 → fvarId = fvarId_1
-- Mathlib.Combinatorics.Enumerative.Stirling
Nat.stirlingSecond_succ_right : ∀ (n k : ℕ), n ≠ 0 → n.stirlingSecond (k + 1) = (k + 1) * (n - 1).stirlingSecond (k + 1) + (n - 1).stirlingSecond k
-- Mathlib.Topology.Separation.Basic
disjoint_nhds_nhds_iff_not_specializes : ∀ {X : Type u_1} [inst : TopologicalSpace X] [R1Space X] {x y : X}, Disjoint (nhds x) (nhds y) ↔ ¬x ⤳ y
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.completeSpace_ker : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₂ : Type u_6}
  [inst_2 : TopologicalSpace M₂] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R₂ M₂] {M' : Type u_9}
  [inst_5 : UniformSpace M'] [CompleteSpace M'] [inst_7 : AddCommMonoid M'] [inst_8 : Module R₁ M'] [T1Space M₂]
  (f : M' →SL[σ₁₂] M₂), CompleteSpace ↥(↑f).ker
-- Lean.Meta.Tactic.ElimInfo
Lean.Meta.instReprCustomEliminators : Repr Lean.Meta.CustomEliminators
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Nat.instMulLeftMono : MulLeftMono ℕ
-- Mathlib.Combinatorics.Matroid.Sum
Matroid.sum'.eq_1 : ∀ {α : Type u_1} {ι : Type u_2} (M : ι → Matroid α),
  Matroid.sum' M = (Matroid.sigma M).mapEquiv (Equiv.sigmaEquivProd ι α)
-- Mathlib.Order.BoundedOrder.Monotone
StrictMono.apply_eq_top_iff : ∀ {α : Type u} {β : Type v} [inst : PartialOrder α] [inst_1 : OrderTop α] [inst_2 : Preorder β] {f : α → β} {a : α},
  StrictMono f → (f a = f ⊤ ↔ a = ⊤)
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenSubgroup.ext_iff : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] {U V : OpenSubgroup G}, U = V ↔ ∀ (x : G), x ∈ U ↔ x ∈ V
-- Mathlib.Algebra.Order.Hom.Monoid
instCoeTCOrderMonoidHomOfOrderHomClassOfMonoidHomClass.eq_1 : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : MulOneClass α]
  [inst_3 : MulOneClass β] [inst_4 : FunLike F α β] [inst_5 : OrderHomClass F α β] [inst_6 : MonoidHomClass F α β],
  instCoeTCOrderMonoidHomOfOrderHomClassOfMonoidHomClass = { coe := OrderMonoidHomClass.toOrderMonoidHom }
-- Mathlib.Analysis.Calculus.FDeriv.CompCLM
HasFDerivAt.continuousAlternatingMap_apply_const : ∀ {𝕜 : 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] {x : E} {ι : Type u_5} {c : E → F [⋀^ι]→L[𝕜] G}
  {c' : E →L[𝕜] F [⋀^ι]→L[𝕜] G} [inst_7 : Fintype ι],
  HasFDerivAt c c' x → ∀ (u : ι → F), HasFDerivAt (fun y => (c y) u) (c'.flipAlternating u) x
-- Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel
CategoryTheory.Abelian.epiWithInjectiveKernel.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C] (x x_1 : C)
  (f : x ⟶ x_1),
  CategoryTheory.Abelian.epiWithInjectiveKernel f =
    (CategoryTheory.Epi f ∧ CategoryTheory.Injective (CategoryTheory.Limits.kernel f))
-- Mathlib.Data.Prod.PProd
PProd.mk.eta : ∀ {α : Sort u_1} {β : Sort u_2} {p : α ×' β}, ⟨p.fst, p.snd⟩ = p
-- Mathlib.Tactic.Eval
/-- `eval% x` evaluates the term `x : X` in the interpreter, and then injects the resulting expression.

As an example:
```lean
example : 2^10 = eval% 2^10 := by
  -- goal is `2^10 = 1024`
  sorry
```
This only works if a `Lean.ToExpr X` instance is available.

Tip: you can use `show_term eval% x` to see the value of `eval% x`.
 -/
Mathlib.Meta.eval_expr : Lean.ParserDescr
-- Mathlib.Tactic.Order.Graph.Basic
/-- State for the DFS algorithm.  -/
Mathlib.Tactic.Order.Graph.DFSState : Type
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
/-- **Alias** of `MonoidAlgebra.symm_mapAddEquiv`. -/
MonoidAlgebra.symm_mapRangeAddEquiv : ∀ {R : Type u_3} {S : Type u_4} {M : Type u_6} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : Mul M] (e : R ≃+ S),
  (MonoidAlgebra.mapAddEquiv M e).symm = MonoidAlgebra.mapAddEquiv M e.symm
-- Init.Grind.AC
Lean.Grind.AC.Seq.sort'.eq_2 : ∀ (acc : Lean.Grind.AC.Seq) (x : Lean.Grind.AC.Var) (s_2 : Lean.Grind.AC.Seq),
  (Lean.Grind.AC.Seq.cons x s_2).sort' acc = s_2.sort' (Lean.Grind.AC.Seq.insert x acc)
-- Mathlib.MeasureTheory.Measure.NullMeasurable
MeasureTheory.NullMeasurableSet.exists_measurable_superset_ae_eq : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α},
  MeasureTheory.NullMeasurableSet s μ → ∃ t ⊇ s, MeasurableSet t ∧ t =ᵐ[μ] s
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.ratCast_def : ∀ {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6}
  {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)]
  [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_3 : IsDirectedOrder ι] [inst_4 : Nonempty ι]
  [inst_5 : (i : ι) → DivisionRing (G i)] [inst_6 : ∀ (i j : ι) (h : i ≤ j), RingHomClass (T h) (G i) (G j)] (q : ℚ)
  (i : ι), ↑q = ⟦⟨i, ↑q⟩⟧
-- Mathlib.Algebra.BigOperators.Finprod
finprod_def' : ∀ {M : Type u_7} {α : Sort u_8} [inst : CommMonoid M] (f : α → M),
  finprod f = if h : Function.HasFiniteMulSupport (f ∘ PLift.down) then ∏ i ∈ Set.Finite.toFinset h, f i.down else 1
-- Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
MeasureTheory.MemLp.mul : ∀ {α : Type u_1} {x : MeasurableSpace α} {𝕜 : Type u_2} [inst : NormedRing 𝕜] {μ : MeasureTheory.Measure α}
  {p q r : ENNReal} {f φ : α → 𝕜},
  MeasureTheory.MemLp f q μ → MeasureTheory.MemLp φ p μ → ∀ [hpqr : p.HolderTriple q r], MeasureTheory.MemLp (φ * f) r μ
-- Mathlib.Algebra.Group.Hom.Defs
ZeroHom.id.eq_1 : ∀ (M : Type u_10) [inst : Zero M], ZeroHom.id M = { toFun := fun x => x, map_zero' := ⋯ }
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.getKey_ofList_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {l : List (α × β)} {k k' : α},
  (k == k') = true →
    List.Pairwise (fun a b => (a.1 == b.1) = false) l →
      k ∈ List.map Prod.fst l →
        ∀ {h : k' ∈ Std.ExtDHashMap.Const.ofList l}, (Std.ExtDHashMap.Const.ofList l).getKey k' h = k
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBSet.mem_toList_insert : ∀ {α : Type u_1} {cmp : α → α → Ordering} {v v' : α} [Std.TransCmp cmp] {t : RBTree.RBSet α cmp},
  v' ∈ (t.insert v).toList ↔ v' ∈ t.toList ∧ t.find? v ≠ some v' ∨ v' = v
-- Mathlib.GroupTheory.Nilpotent
/-- **Alias** of `Subgroup.is_ascending_rev_series_of_is_descending`. -/
is_ascending_rev_series_of_is_descending : ∀ (G : Type u_1) [inst : Group G] {H : ℕ → Subgroup G} {n : ℕ},
  H n = ⊥ → Subgroup.IsDescendingCentralSeries H → Subgroup.IsAscendingCentralSeries fun m => H (n - m)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.get?_union_of_not_mem_left : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : α → Type v} {m₁ m₂ : Std.DHashMap.Raw α β}
  [inst_2 : LawfulBEq α], m₁.WF → m₂.WF → ∀ {k : α}, k ∉ m₁ → (m₁ ∪ m₂).get? k = m₂.get? k
-- Mathlib.Algebra.Order.Group.Synonym
OrderDual.instAdd.eq_1 : ∀ {α : Type u_1} [inst : Add α], OrderDual.instAdd = inst
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.denote'.go.eq_1 : ∀ (ctx : Int.Internal.Linear.Context) (p : Int.Internal.Linear.Poly),
  Int.Internal.Linear.Poly.denote'.go ctx p =
    Int.Internal.Linear.Poly.rec (motive := fun x => ℤ → ℤ) (fun k r => Bool.rec (r + k) r (k.beq' 0))
      (fun k v x ih r =>
        Bool.rec (ih (r + k * Int.Internal.Linear.Var.denote ctx v)) (ih (r + Int.Internal.Linear.Var.denote ctx v))
          (k.beq' 1))
      p
-- Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
MvPolynomial.universalFactorizationMap.eq_1 : ∀ (R : Type u_1) [inst : CommRing R] (n m k : ℕ) (hn : n = m + k),
  MvPolynomial.universalFactorizationMap R n m k hn =
    (MvPolynomial.mapEquivMonic R (TensorProduct R (MvPolynomial (Fin m) R) (MvPolynomial (Fin k) R)) n).symm
      ⟨↑((MvPolynomial.mapEquivMonic R (TensorProduct R (MvPolynomial (Fin m) R) (MvPolynomial (Fin k) R)) m)
              Algebra.TensorProduct.includeLeft) *
          ↑((MvPolynomial.mapEquivMonic R (TensorProduct R (MvPolynomial (Fin m) R) (MvPolynomial (Fin k) R)) k)
              Algebra.TensorProduct.includeRight),
        ⋯⟩
-- Mathlib.Algebra.BigOperators.Associated
exists_associated_mem_of_dvd_prod : ∀ {M₀ : Type u_3} [inst : CommMonoidWithZero M₀] [IsCancelMulZero M₀] {p : M₀},
  Prime p → ∀ {s : Multiset M₀}, (∀ r ∈ s, Prime r) → p ∣ s.prod → ∃ q ∈ s, Associated p q
-- Init.Data.String.Lemmas.Splits
String.Slice.Pos.Splits.prevn : ∀ {s : String.Slice} {t₁ t₂ : String} {p : s.Pos},
  p.Splits t₁ t₂ →
    ∀ (n : ℕ),
      (p.prevn n).Splits (String.ofList (List.take (t₁.toList.length - n) t₁.toList))
        (String.ofList (List.drop (t₁.toList.length - n) t₁.toList) ++ t₂)
-- Mathlib.RingTheory.Extension.Basic
Algebra.Extension.Hom.mk.injEq : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {P : Algebra.Extension R S}
  {R' : Type u_1} {S' : Type u_2} [inst_3 : CommRing R'] [inst_4 : CommRing S'] [inst_5 : Algebra R' S']
  {P' : Algebra.Extension R' S'} [inst_6 : Algebra R R'] [inst_7 : Algebra S S'] (toRingHom : P.Ring →+* P'.Ring)
  (toRingHom_algebraMap :
    ∀ (x : R), toRingHom ((algebraMap R P.Ring) x) = (algebraMap R' P'.Ring) ((algebraMap R R') x))
  (algebraMap_toRingHom :
    ∀ (x : P.Ring), (algebraMap P'.Ring S') (toRingHom x) = (algebraMap S S') ((algebraMap P.Ring S) x))
  (toRingHom_1 : P.Ring →+* P'.Ring)
  (toRingHom_algebraMap_1 :
    ∀ (x : R), toRingHom_1 ((algebraMap R P.Ring) x) = (algebraMap R' P'.Ring) ((algebraMap R R') x))
  (algebraMap_toRingHom_1 :
    ∀ (x : P.Ring), (algebraMap P'.Ring S') (toRingHom_1 x) = (algebraMap S S') ((algebraMap P.Ring S) x)),
  ({ toRingHom := toRingHom, toRingHom_algebraMap := toRingHom_algebraMap,
        algebraMap_toRingHom := algebraMap_toRingHom } =
      { toRingHom := toRingHom_1, toRingHom_algebraMap := toRingHom_algebraMap_1,
        algebraMap_toRingHom := algebraMap_toRingHom_1 }) =
    (toRingHom = toRingHom_1)
-- Mathlib.CategoryTheory.Monad.Kleisli
CategoryTheory.Kleisli.instInhabited : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [Inhabited C] → (T : CategoryTheory.Monad C) → Inhabited (CategoryTheory.Kleisli T)
-- Mathlib.Analysis.Convex.Star
/-- The image of a star-convex set under an affine map is star-convex.  -/
StarConvex.affine_image : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : Ring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : AddCommGroup F] [inst_4 : Module 𝕜 E] [inst_5 : Module 𝕜 F] {x : E} (f : E →ᵃ[𝕜] F) {s : Set E},
  StarConvex 𝕜 x s → StarConvex 𝕜 (f x) (⇑f '' s)
-- Mathlib.RingTheory.Extension.Presentation.Basic
Algebra.Presentation.localizationAway_dimension_zero : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (r : R)
  [inst_3 : IsLocalization.Away r S], (Algebra.Presentation.localizationAway S r).dimension = 0
-- Mathlib.AlgebraicTopology.RelativeCellComplex.AttachCells
HomotopicalAlgebra.AttachCells.cell_def_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {α : Type t} {A B : α → C} {g : (a : α) → A a ⟶ B a}
  {X₁ X₂ : C} {f : X₁ ⟶ X₂} (c : HomotopicalAlgebra.AttachCells g f) (i : c.ι) {Z : C} (h : X₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (c.cell i) h =
    CategoryTheory.CategoryStruct.comp (c.cofan₂.inj i) (CategoryTheory.CategoryStruct.comp c.g₂ h)
-- Mathlib.Computability.TuringMachine.Computable
/-- A forgetful map, forgetting that the time function is polynomial.  -/
Turing.TM2ComputableInPolyTime.toTM2ComputableInTime : {α β αΓ βΓ : Type} →
  {ea : α → List αΓ} →
    {eb : β → List βΓ} → {f : α → β} → Turing.TM2ComputableInPolyTime ea eb f → Turing.TM2ComputableInTime ea eb f
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.SInt
Int16.reduceLT : Lean.Meta.Simp.Simproc
-- Mathlib.CategoryTheory.Sites.Point.Basic
/-- the fiber functor on the underlying category of the site  -/
CategoryTheory.GrothendieckTopology.Point.fiber : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.GrothendieckTopology C} → J.Point → CategoryTheory.Functor C (Type w)
-- Mathlib.Order.Filter.AtTopBot.Interval
Finset.tendsto_Ioc_neg_atTop_atTop : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α]
  [inst_3 : LocallyFiniteOrder α] [NoBotOrder α], Filter.Tendsto (fun a => Finset.Ioc (-a) a) Filter.atTop Filter.atTop
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.toCLM_apply_eq_sum : ∀ {m : Type u_1} {n : Type u_2} {A : Type u_5} [inst : Fintype m] [inst_1 : NonUnitalCStarAlgebra A]
  {M : CStarMatrix m n A} {v : WithCStarModule A (m → A)},
  (CStarMatrix.toCLM M) v = (WithCStarModule.equiv A (n → A)).symm fun j => ∑ i, v i * M i j
-- Mathlib.RingTheory.Coalgebra.CoassocSimps
_private.Mathlib.RingTheory.Coalgebra.CoassocSimps.0.CoassocSimps.termα : Lean.ParserDescr
-- Mathlib.MeasureTheory.Covering.Vitali
/-- The measurable **Vitali covering theorem**.

Assume one is given a family `t` of closed sets with nonempty interior, such that each `a ∈ t` is
included in a ball `B (x, r)` and covers a definite proportion of the ball `B (x, 3 r)` for a given
measure `μ` (think of the situation where `μ` is a doubling measure and `t` is a family of balls).
Consider a (possibly non-measurable) set `s` at which the family is fine, i.e., every point of `s`
belongs to arbitrarily small elements of `t`. Then one can extract from `t` a disjoint subfamily
that covers almost all `s`.

For more flexibility, we give a statement with a parameterized family of sets.
 -/
Vitali.exists_disjoint_covering_ae : ∀ {α : Type u_1} {ι : Type u_2} [inst : PseudoMetricSpace α] [inst_1 : MeasurableSpace α] [OpensMeasurableSpace α]
  [SecondCountableTopology α] (μ : MeasureTheory.Measure α) [MeasureTheory.IsLocallyFiniteMeasure μ] (s : Set α)
  (t : Set ι) (C : NNReal) (r : ι → ℝ) (c : ι → α) (B : ι → Set α),
  (∀ a ∈ t, B a ⊆ Metric.closedBall (c a) (r a)) →
    (∀ a ∈ t, μ (Metric.closedBall (c a) (3 * r a)) ≤ ↑C * μ (B a)) →
      (∀ a ∈ t, (interior (B a)).Nonempty) →
        (∀ a ∈ t, IsClosed (B a)) →
          (∀ x ∈ s, ∀ ε > 0, ∃ a ∈ t, r a ≤ ε ∧ c a = x) →
            ∃ u ⊆ t, u.Countable ∧ u.PairwiseDisjoint B ∧ μ (s \ ⋃ a ∈ u, B a) = 0
-- Mathlib.Algebra.Group.Subgroup.Lattice
Subgroup.closure_union : ∀ {G : Type u_1} [inst : Group G] (s t : Set G), Subgroup.closure (s ∪ t) = Subgroup.closure s ⊔ Subgroup.closure t
-- Mathlib.LinearAlgebra.Multilinear.Pi
MultilinearMap.piFamily_apply : ∀ {ι : Type uι} {κ : ι → Type uκ} {R : Type uR} {M : (i : ι) → κ i → Type uM} {N : ((i : ι) → κ i) → Type uN}
  [inst : Semiring R] [inst_1 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)]
  [inst_2 : (p : (i : ι) → κ i) → AddCommMonoid (N p)] [inst_3 : (i : ι) → (k : κ i) → Module R (M i k)]
  [inst_4 : (p : (i : ι) → κ i) → Module R (N p)]
  (f : (p : (i : ι) → κ i) → MultilinearMap R (fun i => M i (p i)) (N p)) (x : (i : ι) → (j : κ i) → M i j)
  (p : (i : ι) → κ i), (MultilinearMap.piFamily f) x p = (f p) fun i => x i (p i)
-- Mathlib.Analysis.Complex.ReImTopology
Complex.frontier_setOfPred_lt_im : ∀ (a : ℝ), frontier {z | a < z.im} = {z | z.im = a}
-- Mathlib.Algebra.Star.LinearMap
Module.End.IsUnit.intrinsicStar : ∀ {R : Type u_1} {E : Type u_2} [inst : Semiring R] [inst_1 : InvolutiveStar R] [inst_2 : AddCommMonoid E]
  [inst_3 : Module R E] [inst_4 : StarAddMonoid E] [inst_5 : StarModule R E] {f : WithConv (Module.End R E)},
  IsUnit f.ofConv → IsUnit (star f).ofConv
-- Mathlib.Data.Finsupp.Ext
Finsupp.mulHom_ext'_iff : ∀ {α : Type u_1} {M : Type u_2} {N : Type u_3} [inst : AddZeroClass M] [inst_1 : MulOneClass N]
  {f g : Multiplicative (α →₀ M) →* N},
  f = g ↔
    ∀ (x : α),
      f.comp (AddMonoidHom.toMultiplicative (Finsupp.singleAddHom x)) =
        g.comp (AddMonoidHom.toMultiplicative (Finsupp.singleAddHom x))
-- Mathlib.Analysis.SpecificLimits.Normed
isLittleO_pow_pow_of_lt_left : ∀ {r₁ r₂ : ℝ}, 0 ≤ r₁ → r₁ < r₂ → (fun n => r₁ ^ n) =o[Filter.atTop] fun n => r₂ ^ n
-- Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
Equiv.Perm.count_le_one_of_centralizer_le_alternating : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {g : Equiv.Perm α},
  Subgroup.centralizer {g} ≤ alternatingGroup α → ∀ (i : ℕ), Multiset.count i g.cycleType ≤ 1
-- Mathlib.Topology.Separation.Basic
injective_nhdsSet : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T1Space X], Function.Injective nhdsSet
-- Mathlib.Analysis.Calculus.Deriv.Prod
/-- A variant of `hasDerivAt_finCons` where the derivative variables are free on the RHS
instead.  -/
hasDerivAt_finCons' : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {n : ℕ} {F' : Fin n.succ → Type u_1}
  [inst_1 : (i : Fin n.succ) → NormedAddCommGroup (F' i)] [inst_2 : (i : Fin n.succ) → NormedSpace 𝕜 (F' i)]
  {φ : 𝕜 → F' 0} {φs : 𝕜 → (i : Fin n) → F' i.succ} {φ' : F' 0} {φs' : (i : Fin n) → F' i.succ},
  HasDerivAt (fun x => Fin.cons (φ x) (φs x)) (Fin.cons φ' φs') x ↔ HasDerivAt φ φ' x ∧ HasDerivAt φs φs' x
-- Aesop.Script.OptimizeSyntax
Aesop.optimizeFocusRenameI : {m : Type → Type} → [Monad m] → [Lean.MonadQuotation m] → Lean.Syntax → m Lean.Syntax
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.insertMany_list_eq_foldl : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {l : List ((a : α) × β a)},
  m.insertMany l = List.foldl (fun acc p => acc.insert p.fst p.snd) m l
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
CategoryTheory.Limits.reflectsLimit_subsingleton : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J] (K : CategoryTheory.Functor J C)
  (F : CategoryTheory.Functor C D), Subsingleton (CategoryTheory.Limits.ReflectsLimit K F)
-- Mathlib.Algebra.Category.ModuleCat.FilteredColimits
/-- The "unlifted" version of scalar multiplication in the colimit.  -/
ModuleCat.FilteredColimits.colimitSMulAux : {R : Type u} →
  [inst : Ring R] →
    {J : Type v} →
      [inst_1 : CategoryTheory.SmallCategory J] →
        [inst_2 : CategoryTheory.IsFiltered J] →
          (F : CategoryTheory.Functor J (ModuleCat R)) → R → (j : J) × ↑(F.obj j) → ↑(ModuleCat.FilteredColimits.M F)
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.aeval_smul : ∀ {R : Type u} {A : Type z} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (f : Polynomial R)
  {G : Type u_3} [inst_3 : Monoid G] [inst_4 : MulSemiringAction G A] [SMulCommClass G R A] (g : G) (x : A),
  (Polynomial.aeval (g • x)) f = g • (Polynomial.aeval x) f
-- Mathlib.Algebra.Order.Star.Basic
SelfAdjointDecompose.mk : ∀ {R : Type u_3} [inst : AddGroup R] [inst_1 : Star R] [inst_2 : PartialOrder R],
  (∀ {a : R}, IsSelfAdjoint a → ∃ b c, 0 ≤ b ∧ 0 ≤ c ∧ a = b - c) → SelfAdjointDecompose R
-- Mathlib.Order.Filter.Basic
Filter.EventuallyEq.congr_left : ∀ {α : Type u} {β : Type v} {l : Filter α} {f g h : α → β}, f =ᶠ[l] g → (f =ᶠ[l] h ↔ g =ᶠ[l] h)
-- Mathlib.Analysis.Normed.Operator.Perturbation.StrictByFinite
/-- If two linear maps `u, v : E → F` differ by a finite rank linear map (recall that this is
denoted `u.toLinearMap ≈ v.toLinearMap` in scope `LinearMap.FiniteRangeSetoid`), then `u` is
strict with closed range if and only if `v` is strict with closed range.

This is [N. Bourbaki, *Théories Spectrales*, Chapitre III, § 3, n° 1, Cor. 1][bourbaki2023].  -/
ContinuousLinearMap.isStrictMap_isClosed_range_iff_of_finiteRangeSetoid : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] {E : Type u_2} {F : Type u_3}
  [inst_2 : AddCommGroup E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] [inst_9 : TopologicalSpace F]
  [IsTopologicalAddGroup F] [ContinuousSMul 𝕜 F] [T2Space F] (u v : E →L[𝕜] F),
  ↑u ≈ ↑v → (Topology.IsStrictMap ⇑u ∧ IsClosed ↑(↑u).range ↔ Topology.IsStrictMap ⇑v ∧ IsClosed ↑(↑v).range)