mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup
spinGroup.coe_star_mul_self : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} (x : ↥(spinGroup Q)), star ↑x * ↑x = 1
-- Mathlib.Analysis.Calculus.MeanValue
/-- If two functions have equal Fréchet derivatives at every point of a convex set, and are equal at
one point in that set, then they are equal on that set.  -/
Convex.eqOn_of_fderivWithin_eq : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {𝕜 : Type u_3} {G : Type u_4}
  [inst_2 : NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] [inst_4 : NormedSpace 𝕜 E]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f g : E → G} {s : Set E} {x : E},
  Convex ℝ s →
    DifferentiableOn 𝕜 f s →
      DifferentiableOn 𝕜 g s →
        UniqueDiffOn 𝕜 s → Set.EqOn (fderivWithin 𝕜 f s) (fderivWithin 𝕜 g s) s → x ∈ s → f x = g x → Set.EqOn f g s
-- Mathlib.MeasureTheory.Measure.NullMeasurable
MeasurableSet.nullMeasurableSet : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α},
  MeasurableSet s → MeasureTheory.NullMeasurableSet s μ
-- Mathlib.Algebra.Order.Monoid.Submonoid
Submonoid.oneLE.eq_1 : ∀ (M : Type u_1) [inst : Monoid M] [inst_1 : Preorder M] [inst_2 : MulLeftMono M],
  Submonoid.oneLE M = { carrier := Set.Ici 1, mul_mem' := ⋯, one_mem' := ⋯ }
-- Init.Data.UInt.Bitwise
UInt32.ofNatLT_and : ∀ (a b : ℕ) (ha : a < 2 ^ 32) (hb : b < 2 ^ 32),
  UInt32.ofNatLT (a &&& b) ⋯ = UInt32.ofNatLT a ha &&& UInt32.ofNatLT b hb
-- Mathlib.LinearAlgebra.TensorProduct.Tower
/-- `B`-linear equivalence between `M ⊗[A] (A ⊗[R] N)` and `M ⊗[R] N`.
In particular useful with `B = A`.  -/
TensorProduct.AlgebraTensorModule.cancelBaseChange : (R : Type uR) →
  (A : Type uA) →
    (B : Type uB) →
      (M : Type uM) →
        (N : Type uN) →
          [inst : CommSemiring R] →
            [inst_1 : CommSemiring A] →
              [inst_2 : Semiring B] →
                [inst_3 : Algebra R A] →
                  [inst_4 : Algebra R B] →
                    [inst_5 : AddCommMonoid M] →
                      [inst_6 : Module R M] →
                        [inst_7 : Module A M] →
                          [inst_8 : Module B M] →
                            [IsScalarTower R A M] →
                              [inst_10 : IsScalarTower R B M] →
                                [inst_11 : SMulCommClass A B M] →
                                  [inst_12 : AddCommMonoid N] →
                                    [inst_13 : Module R N] →
                                      [inst_14 : Algebra A B] →
                                        [IsScalarTower A B M] →
                                          TensorProduct A M (TensorProduct R A N) ≃ₗ[B] TensorProduct R M N
-- Mathlib.CategoryTheory.ComposableArrows.Basic
/-- The functor `ComposableArrows C n ⥤ ComposableArrows D n` obtained by postcomposition
with a functor `C ⥤ D`.  -/
CategoryTheory.Functor.mapComposableArrows : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {D : Type u_2} →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        CategoryTheory.Functor C D →
          (n : ℕ) → CategoryTheory.Functor (CategoryTheory.ComposableArrows C n) (CategoryTheory.ComposableArrows D n)
-- Mathlib.Data.EReal.Operations
EReal.right_distrib_of_nonneg : ∀ {a b c : EReal}, 0 ≤ a → 0 ≤ b → (a + b) * c = a * c + b * c
-- Mathlib.Algebra.Polynomial.Derivative
Polynomial.derivative_C_mul_X_sq : ∀ {R : Type u} [inst : Semiring R] (a : R),
  Polynomial.derivative (Polynomial.C a * Polynomial.X ^ 2) = Polynomial.C (a * 2) * Polynomial.X
-- Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
MeasurableSet.sup_eq_union : ∀ {α : Type u_1} [inst : MeasurableSpace α] (s t : { s // MeasurableSet s }), s ⊔ t = s ∪ t
-- Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Matrix.IsAdjMatrix.toGraphReindexIso_symm_apply : ∀ {α : Type u_1} {V : Type u_2} {W : Type u_3} (A : Matrix V V α) [inst : MulZeroOneClass α] [inst_1 : Nontrivial α]
  (h : A.IsAdjMatrix) (f : V ≃ W) (a : V), (RelIso.symm (Matrix.IsAdjMatrix.toGraphReindexIso A h f)) a = f a
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
contDiffOn_tsum_cexp : ∀ (k : ℕ∞),
  ContDiffOn ℂ (↑k) (fun z => ∑' (n : ℕ), Complex.exp (2 * ↑Real.pi * Complex.I * z) ^ n)
    UpperHalfPlane.upperHalfPlaneSet
-- Lean.Data.Lsp.Basic
Lean.Lsp.WorkDoneProgressEnd.mk.sizeOf_spec : ∀ (kind : String) (message? : Option String),
  sizeOf { kind := kind, message? := message? } = 1 + sizeOf kind + sizeOf message?
-- Mathlib.MeasureTheory.Integral.IntegrableOn
MeasureTheory.integrableOn_singleton : ∀ {α : Type u_1} {ε' : Type u_4} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : TopologicalSpace ε']
  [inst_1 : ESeminormedAddMonoid ε'] {f : α → ε'} {x : α} [MeasurableSingletonClass α],
  autoParam (‖f x‖ₑ ≠ ⊤) MeasureTheory.integrableOn_singleton._auto_1 →
    autoParam (μ {x} < ⊤) MeasureTheory.integrableOn_singleton._auto_3 → MeasureTheory.IntegrableOn f {x} μ
-- Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
MeasureTheory.Measure.measurable_rnDeriv : ∀ {α : Type u_1} {m : MeasurableSpace α} (μ ν : MeasureTheory.Measure α), Measurable (μ.rnDeriv ν)
-- Mathlib.Topology.Algebra.Group.Defs
IsTopologicalGroup.toContinuousInv : ∀ {G : Type u_4} {inst : TopologicalSpace G} {inst_1 : Group G} [self : IsTopologicalGroup G], ContinuousInv G
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
/-- If `f` satisfies a boundedness property around `0`, one can deduce a bound on `f m₁ - f m₂`
using the multilinearity. Here, we give a usable but not very precise version. See
`norm_image_sub_le_of_bound'` for a more precise but less usable version. The bound is
`‖f m - f m'‖ ≤ C * card ι * ‖m - m'‖ * (max ‖m‖ ‖m'‖) ^ (card ι - 1)`.  -/
MultilinearMap.norm_image_sub_le_of_bound : ∀ {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)]
  [inst_3 : SeminormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] [inst_5 : Fintype ι] (f : MultilinearMap 𝕜 E G)
  {C : ℝ},
  0 ≤ C →
    (∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i, ‖m i‖) →
      ∀ (m₁ m₂ : (i : ι) → E i),
        ‖f m₁ - f m₂‖ ≤ C * ↑(Fintype.card ι) * max ‖m₁‖ ‖m₂‖ ^ (Fintype.card ι - 1) * ‖m₁ - m₂‖
-- Mathlib.RingTheory.Ideal.Maps
RingHom.ker_eq_comap_bot : ∀ {R : Type u} {S : Type v} {F : Type u_1} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : FunLike F R S]
  [rcf : RingHomClass F R S] (f : F), RingHom.ker f = Ideal.comap f ⊥
-- Mathlib.Algebra.Algebra.Operations
Submodule.comap_op_one : ∀ {R : Type u} [inst : CommSemiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Algebra R A],
  Submodule.comap (↑(MulOpposite.opLinearEquiv R)) 1 = 1
-- Mathlib.RingTheory.Extension.Presentation.Submersive
Algebra.PreSubmersivePresentation.localizationAway_jacobiMatrix : ∀ {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.PreSubmersivePresentation.localizationAway S r).jacobiMatrix = Matrix.diagonal fun x => MvPolynomial.C r
-- Mathlib.Topology.Algebra.Constructions
AddOpposite.continuous_unop : ∀ {M : Type u_1} [inst : TopologicalSpace M], Continuous AddOpposite.unop
-- Lean.DocString.Markdown
Lean.Doc.instMarkdownInlineElabInline : Lean.Doc.MarkdownInline Lean.ElabInline
-- Lean.Data.Options
Lean.OptionDeprecation.mk.inj : ∀ {since : String} {text? : Option String} {since_1 : String} {text?_1 : Option String},
  { since := since, text? := text? } = { since := since_1, text? := text?_1 } → since = since_1 ∧ text? = text?_1
-- Lean.Meta.Tactic.Grind.Types
/-- Returns the number of theorem instances generated so far.  -/
Lean.Meta.Grind.getNumTheoremInstances : Lean.Meta.Grind.GoalM ℕ
-- Mathlib.Combinatorics.Configuration
Configuration.ofField.instNondegenerateProjectivizationForallFinOfNatNat : ∀ {K : Type u_3} [inst : Field K],
  Configuration.Nondegenerate (Projectivization K (Fin 3 → K)) (Projectivization K (Fin 3 → K))
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
MeasureTheory.JordanDecomposition.neg_posPart : ∀ {α : Type u_1} [inst : MeasurableSpace α] (j : MeasureTheory.JordanDecomposition α), (-j).posPart = j.negPart
-- Mathlib.AlgebraicTopology.SimplicialSet.SubcomplexEvaluation
Preorder.colimitCoconeOfIsLUB.congr_simp : ∀ {C : Type u} [inst : Preorder C] {J : Type u'} [inst_1 : CategoryTheory.Category.{v, u'} J]
  (F : CategoryTheory.Functor J C) {pt pt_1 : C} (e_pt : pt = pt_1) (h : IsLUB (Set.range F.obj) pt),
  Preorder.colimitCoconeOfIsLUB F h = Preorder.colimitCoconeOfIsLUB F ⋯
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.EqCnstr.mk : Int.Internal.Linear.Poly → Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof → Lean.Meta.Grind.Arith.Cutsat.EqCnstr
-- Mathlib.Order.ULift
ULift.instMin_mathlib.eq_1 : ∀ {α : Type u} [inst : Min α], ULift.instMin_mathlib = { min := fun x y => { down := x.down ⊓ y.down } }
-- Mathlib.Data.PFunctor.Univariate.Basic
PFunctor.Obj.iget.eq_1 : ∀ {P : PFunctor.{uA, uB}} [inst : DecidableEq P.A] {α : Type u_1} [inst_1 : Inhabited α] (x : ↑P α) (i : P.Idx),
  x.iget i = if h : i.fst = x.fst then x.snd (cast ⋯ i.snd) else default
-- Mathlib.Topology.Category.Profinite.Nobeling.Basic
Profinite.NobelingProof.Products.rel_head!_of_mem : ∀ {I : Type u} [inst : LinearOrder I] [inst_1 : Inhabited I] {i : I} {l : Profinite.NobelingProof.Products I},
  i ∈ ↑l → i ≤ (↑l).head!
-- Mathlib.Data.Complex.Basic
Complex.ofReal_ofScientific : ∀ (m : ℕ) (s : Bool) (e : ℕ), ↑(OfScientific.ofScientific m s e) = OfScientific.ofScientific m s e
-- Mathlib.RingTheory.Polynomial.Content
Polynomial.IsPrimitive.dvd_primPart_iff_dvd : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : NormalizedGCDMonoid R] {p q : Polynomial R},
  p.IsPrimitive → q ≠ 0 → (p ∣ q.primPart ↔ p ∣ q)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.mulMon_nc.eq_1 : ∀ (k : ℤ) (m : Lean.Grind.CommRing.Mon) (p : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.Poly.mulMon_nc k m p =
    bif k == 0 then Lean.Grind.CommRing.Poly.num 0
    else
      bif m == Lean.Grind.CommRing.Mon.unit then Lean.Grind.CommRing.Poly.mulConst k p
      else Lean.Grind.CommRing.Poly.mulMon_nc.go k m p (Lean.Grind.CommRing.Poly.num 0)
-- Mathlib.CategoryTheory.Sites.Limits
CategoryTheory.Sheaf.sheafifyCocone_ι_app_val : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w}
  [inst_1 : CategoryTheory.Category.{w', w} D] {K : Type z} [inst_2 : CategoryTheory.Category.{z', z} K]
  [inst_3 : CategoryTheory.HasWeakSheafify J D] {F : CategoryTheory.Functor K (CategoryTheory.Sheaf J D)}
  (E : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.sheafToPresheaf J D))) (k : K),
  ((CategoryTheory.Sheaf.sheafifyCocone E).ι.app k).hom =
    CategoryTheory.CategoryStruct.comp (E.ι.app k) (CategoryTheory.toSheafify J E.pt)
-- Mathlib.SetTheory.Ordinal.Notation
ONote.mul_nf : ∀ (o₁ o₂ : ONote) [o₁.NF] [o₂.NF], (o₁ * o₂).NF
-- Mathlib.Data.Matrix.Basic
/-- `Matrix.diag` as an `AddMonoidHom`.  -/
Matrix.diagAddMonoidHom : (n : Type u_3) → (α : Type u_11) → [inst : AddZeroClass α] → Matrix n n α →+ n → α
-- Mathlib.Tactic.NormNum.Ordinal
Mathlib.Meta.NormNum.isNat_ordinalLT_true : ∀ {a b : Ordinal.{u}} {an bn : ℕ},
  Mathlib.Meta.NormNum.IsNat a an → Mathlib.Meta.NormNum.IsNat b bn → decide (an < bn) = true → a < b
-- Init.Data.Nat.Gcd
Nat.gcd_le_right : ∀ {n : ℕ} (m : ℕ), 0 < n → m.gcd n ≤ n
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
CochainComplex.mappingCone.map_inr : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v, u_1} C]
  [inst_1 : CategoryTheory.Category.{v', u_2} D] [inst_2 : CategoryTheory.Preadditive C]
  [inst_3 : CategoryTheory.Preadditive D] {F G : CochainComplex C ℤ} (φ : F ⟶ G)
  [inst_4 : HomologicalComplex.HasHomotopyCofiber φ] (H : CategoryTheory.Functor C D) [inst_5 : H.Additive]
  [inst_6 : HomologicalComplex.HasHomotopyCofiber ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)],
  CategoryTheory.CategoryStruct.comp
      ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map (CochainComplex.mappingCone.inr φ))
      (CochainComplex.mappingCone.mapHomologicalComplexIso φ H).hom =
    CochainComplex.mappingCone.inr ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)
-- Mathlib.CategoryTheory.Presentable.Directed
CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.ext : ∀ {J : Type w} {inst : CategoryTheory.SmallCategory J} {κ : Cardinal.{w}}
  {x y : CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram J κ}, x.W = y.W → x.P = y.P → x = y
-- Init.Data.Array.Find
Array.findSome?_replicate_of_isSome : ∀ {α : Type u_1} {α_1 : Type u_2} {f : α → Option α_1} {n : ℕ} {a : α},
  (f a).isSome = true → Array.findSome? f (Array.replicate n a) = if n = 0 then none else f a
-- Lean.Elab.Tactic.RCases
/-- This will match a list of patterns against a list of hypotheses `e`. The arguments are similar
to `rcasesCore`, but the patterns and local variables are in `pats`. Because the calls are all
nested in continuations, later arguments can be matched many times, once per goal produced by
earlier arguments. For example `⟨a | b, ⟨c, d⟩⟩` performs the `⟨c, d⟩` match twice, once on the
`a` branch and once on `b`.
 -/
_private.Lean.Elab.Tactic.RCases.0.Lean.Elab.Tactic.RCases.rcasesContinue : {α : Type} →
  Lean.MVarId →
    Lean.Meta.FVarSubst →
      Array Lean.FVarId →
        α →
          List (Lean.Elab.Tactic.RCases.RCasesPatt × Lean.Expr) →
            (Lean.MVarId → Lean.Meta.FVarSubst → Array Lean.FVarId → α → Lean.Elab.TermElabM α) → Lean.Elab.TermElabM α
-- Mathlib.SetTheory.Ordinal.Notation
ONote.cmp.eq_def : ∀ (x x_1 : ONote),
  x.cmp x_1 =
    match x, x_1 with
    | ONote.zero, ONote.zero => Ordering.eq
    | x, ONote.zero => Ordering.gt
    | ONote.zero, x => Ordering.lt
    | _o₁@h:(e₁.oadd n₁ a₁), _o₂@h_1:(e₂.oadd n₂ a₂) => (e₁.cmp e₂).then ((cmp ↑n₁ ↑n₂).then (a₁.cmp a₂))
-- Lean.Compiler.CSimpAttr
Lean.Compiler.CSimp.State.mk : Lean.SMap Lean.Name Lean.Compiler.CSimp.Entry → Lean.SSet Lean.Name → Lean.Compiler.CSimp.State
-- Mathlib.Data.Sym.Basic
Sym.map_map : ∀ {α : Type u_3} {β : Type u_4} {γ : Type u_5} {n : ℕ} (g : β → γ) (f : α → β) (s : Sym α n),
  Sym.map g (Sym.map f s) = Sym.map (g ∘ f) s
-- Lean.Meta.Sym.Apply
/-- Precomputed pattern for efficient unification.  -/
Lean.Meta.Sym.BackwardRule.pattern : Lean.Meta.Sym.BackwardRule → Lean.Meta.Sym.Pattern
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.symm_symm : ∀ {R : Type u_4} {S : Type u_5} [inst : Mul R] [inst_1 : Mul S] [inst_2 : Add R] [inst_3 : Add S] (e : R ≃+* S),
  e.symm.symm = e
-- Mathlib.Topology.Semicontinuity.Basic
UpperSemicontinuous.isClosed_preimage : ∀ {α : Type u_1} [inst : TopologicalSpace α] {γ : Type u_4} [inst_1 : LinearOrder γ] {f : α → γ},
  UpperSemicontinuous f → ∀ (y : γ), IsClosed (f ⁻¹' Set.Ici y)
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
CategoryTheory.OverPresheafAux.OverArrows.map₁_map₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A F G : CategoryTheory.Functor Cᵒᵖ (Type v)} {η : F ⟶ A}
  {μ : G ⟶ A} (ε : F ⟶ G) (hε : CategoryTheory.CategoryStruct.comp ε μ = η) {X Y : C}
  {s : CategoryTheory.yoneda.obj X ⟶ A} {t : CategoryTheory.yoneda.obj Y ⟶ A} (f : X ⟶ Y)
  (hf : CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map f) t = s)
  (u : CategoryTheory.OverPresheafAux.OverArrows η t), (u.map₁ ε hε).map₂ f hf = (u.map₂ f hf).map₁ ε hε
-- Lean.Meta.Sym.Pattern
Lean.Meta.Sym.mkPatternFromExpr : Lean.Expr → optParam (List Lean.Name) [] → optParam (Option ℕ) none → Lean.MetaM Lean.Meta.Sym.Pattern
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.contains_eq_isSome_get? : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {a : α}, m.contains a = (Std.ExtDHashMap.Const.get? m a).isSome
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
/-- `cons (exp, coef) tl` approximates `f` when `coef` approximates some function `fC`, `f` is
majorized with exponent `exp` by `basis_hd`, and `tl` approximates `f - fC * basis_hd ^ exp`.  -/
Tactic.ComputeAsymptotics.MultiseriesExpansion.Approximates.cons : ∀ {basis_hd f : ℝ → ℝ} {basis_tl : Tactic.ComputeAsymptotics.Basis} {exp : ℝ}
  {coef : Tactic.ComputeAsymptotics.MultiseriesExpansion basis_tl}
  {tl : Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl},
  coef.Approximates →
    Tactic.ComputeAsymptotics.Majorized f basis_hd exp →
      (Tactic.ComputeAsymptotics.MultiseriesExpansion.mk tl (f - basis_hd ^ exp * coef.toFun)).Approximates →
        (Tactic.ComputeAsymptotics.MultiseriesExpansion.mk
            (Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.cons exp coef tl) f).Approximates
-- Mathlib.FieldTheory.PurelyInseparable.Basic
IsPurelyInseparable.inseparable : ∀ (F : Type u_1) {E : Type u_2} [inst : CommRing F] [inst_1 : Ring E] [inst_2 : Algebra F E] [IsPurelyInseparable F E]
  (x : E), IsSeparable F x → x ∈ (algebraMap F E).range
-- Mathlib.Data.Set.Card
/-- **Alias** of `Set.InjOn.ncard_image`. -/
Set.ncard_image_of_injOn : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β}, Set.InjOn f s → (f '' s).ncard = s.ncard
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.LeftHomologyData.cyclesIso_hom_comp_i : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (h : S.LeftHomologyData) [inst_2 : S.HasLeftHomology],
  CategoryTheory.CategoryStruct.comp h.cyclesIso.hom h.i = S.iCycles
-- Init.Data.Nat.Lemmas
Nat.mod_succ : ∀ (n : ℕ), n % n.succ = n
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- The inverse functor of `ofDiagEquivalence.functor`.  -/
CategoryTheory.CostructuredArrow.ofDiagEquivalence.inverse : {T : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} T] →
    (X : T × T) →
      CategoryTheory.Functor (CategoryTheory.CostructuredArrow (CategoryTheory.Over.forget X.1) X.2)
        (CategoryTheory.CostructuredArrow (CategoryTheory.Functor.diag T) X)
-- Mathlib.Order.Ideal
/-- **Alias** of `Order.Ideal.instPartialOrder`.

---

The partial ordering by subset inclusion, inherited from `Set P`.  -/
Order.Ideal.instPartialOrderIdeal : {P : Type u_1} → [inst : LE P] → PartialOrder (Order.Ideal P)
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.re_coe : ∀ {R : Type u_3} {c₁ c₂ c₃ : R} (x : R) [inst : Zero R], (↑x).re = x
-- Init.Grind.Module.Envelope
Lean.Grind.IntModule.OfNatModule.Q : (α : Type u) → [Lean.Grind.NatModule α] → Type u
-- Mathlib.Analysis.Distribution.TestFunction
TestFunction.instIsSMulApply : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4}
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {n : ℕ∞} {R : Type u_6} [inst_4 : Semiring R]
  [inst_5 : Module R F] [inst_6 : SMulCommClass ℝ R F] [inst_7 : ContinuousConstSMul R F],
  IsSMulApply R (TestFunction Ω F n) E F
-- Mathlib.Algebra.Module.Submodule.Defs
Submodule.toAddSubgroup_inj : ∀ {R : Type u} {M : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] {module_M : Module R M} (p p' : Submodule R M),
  p.toAddSubgroup = p'.toAddSubgroup ↔ p = p'
-- Mathlib.MeasureTheory.Integral.Bochner.Set
/-- If `s` is a countable family of compact sets, `f` is a continuous function, and the sequence
`‖f.restrict (s i)‖ * μ (s i)` is summable, then `f` is integrable on the union of the `s i`.  -/
MeasureTheory.integrableOn_iUnion_of_summable_norm_restrict : ∀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} {ι : Type u_5} [Countable ι] {μ : MeasureTheory.Measure X}
  [inst : NormedAddCommGroup E] [inst_1 : TopologicalSpace X] [BorelSpace X] [T2Space X]
  [MeasureTheory.IsLocallyFiniteMeasure μ] {f : C(X, E)} {s : ι → TopologicalSpace.Compacts X},
  (Summable fun i => ‖ContinuousMap.restrict (↑(s i)) f‖ * μ.real ↑(s i)) →
    MeasureTheory.IntegrableOn (⇑f) (⋃ i, ↑(s i)) μ
-- Mathlib.Analysis.SpecialFunctions.Arsinh
DifferentiableOn.arsinh : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {s : Set E},
  DifferentiableOn ℝ f s → DifferentiableOn ℝ (fun x => Real.arsinh (f x)) s
-- Init.Data.Array.Lemmas
Array.toList_takeWhile : ∀ {α : Type u_1} {p : α → Bool} {as : Array α}, (Array.takeWhile p as).toList = List.takeWhile p as.toList
-- Lean.Meta.Injective
_private.Lean.Meta.Injective.0.Lean.Meta.mkInjectiveEqTheorem : Lean.ConstructorVal → Lean.MetaM Unit
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.HasLimitsOfShape.of_small : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasLimitsOfSize.{v₁, u₁, v, u} C]
  (J : Type u₂) [inst_2 : CategoryTheory.Category.{v₂, u₂} J] [Small.{u₁, u₂} J]
  [CategoryTheory.LocallySmall.{v₁, v₂, u₂} J], CategoryTheory.Limits.HasLimitsOfShape J C
-- Mathlib.Algebra.Order.Archimedean.Class
ArchimedeanOrder.val_of : ∀ {M : Type u_1} (a : M), ArchimedeanOrder.val (ArchimedeanOrder.of a) = a
-- Mathlib.RingTheory.TwoSidedIdeal.Basic
TwoSidedIdeal.setLike : {R : Type u_1} → [inst : NonUnitalNonAssocRing R] → SetLike (TwoSidedIdeal R) R
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- Upgrading a functor `S ⥤ T` to a functor `S ⥤ Over X` and composing with the forgetful functor
`Over X ⥤ T` recovers the original functor.  -/
CategoryTheory.Functor.toOverCompForget : {T : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} T] →
    {S : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} S] →
        (F : CategoryTheory.Functor S T) →
          (X : T) →
            (f : (Y : S) → F.obj Y ⟶ X) →
              (h : ∀ {Y Z : S} (g : Y ⟶ Z), CategoryTheory.CategoryStruct.comp (F.map g) (f Z) = f Y) →
                (F.toOver X f ⋯).comp (CategoryTheory.Over.forget X) ≅ F
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.image_add_const_uIcc : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [IsOrderedAddMonoid α] (a b c : α),
  (fun x => x + a) '' Set.uIcc b c = Set.uIcc (b + a) (c + a)
-- Mathlib.Topology.Algebra.Module.Alternating.Topology
ContinuousAlternatingMap.liftCLM_apply : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_4} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : Module 𝕜 E] [inst_3 : TopologicalSpace E] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] [inst_7 : IsTopologicalAddGroup F] {G : Type u_5} [inst_8 : AddCommGroup G]
  [inst_9 : Module 𝕜 G] [inst_10 : TopologicalSpace G] [inst_11 : ContinuousConstSMul 𝕜 F]
  (f : G →L[𝕜] ContinuousMultilinearMap 𝕜 (fun x => E) F)
  (hf : ∀ (x : G) (v : ι → E) (i j : ι), v i = v j → i ≠ j → (f x) v = 0) (x : G) (v : ι → E),
  ((ContinuousAlternatingMap.liftCLM f hf) x) v = (f x) v
-- Mathlib.Order.Filter.Pointwise
Filter.map_inv : ∀ {α : Type u_2} [inst : Inv α] {f : Filter α}, Filter.map Inv.inv f = f⁻¹
-- Mathlib.Topology.IsLocalHomeomorph
/-- If there is a surjective local homeomorphism between two spaces and one of them is discrete,
then both spaces are discrete.  -/
IsLocalHomeomorph.discreteTopology_iff_of_surjective : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  IsLocalHomeomorph f → Function.Surjective f → (DiscreteTopology X ↔ DiscreteTopology Y)
-- Mathlib.Analysis.SpecificLimits.Basic
tendsto_one_div_atTop_nhds_zero_nat : ∀ {𝕜 : Type u_4} [inst : DivisionSemiring 𝕜] [inst_1 : CharZero 𝕜] [inst_2 : TopologicalSpace 𝕜] [ContinuousSMul ℚ≥0 𝕜],
  Filter.Tendsto (fun n => 1 / ↑n) Filter.atTop (nhds 0)
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.edgeSetEmbedding.eq_1 : ∀ (V : Type u_2), SimpleGraph.edgeSetEmbedding V = OrderEmbedding.ofMapLEIff (fun G => Sym2.fromRel ⋯) ⋯
-- Mathlib.Topology.ClusterPt
clusterPt_lift'_closure_iff : ∀ {X : Type u} [inst : TopologicalSpace X] {x : X} {F : Filter X}, ClusterPt x (F.lift' closure) ↔ ClusterPt x F
-- Mathlib.Algebra.Group.Pointwise.Set.Card
Set.ncard_neg : ∀ {G : Type u_1} [inst : InvolutiveNeg G] (s : Set G), (-s).ncard = s.ncard