mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Localization.SmallShiftedHom
/-- The canonical map `(X ⟶ Y) → SmallShiftedHom.{w} W X Y m₀` when `m₀ = 0` and
`[HasSmallLocalizedShiftedHom.{w} W M X Y]` holds.  -/
CategoryTheory.Localization.SmallShiftedHom.mk₀ : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (W : CategoryTheory.MorphismProperty C) →
      {M : Type w'} →
        [inst_1 : AddMonoid M] →
          [inst_2 : CategoryTheory.HasShift C M] →
            {X Y : C} →
              [inst_3 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X Y] →
                (m₀ : M) → m₀ = 0 → (X ⟶ Y) → CategoryTheory.Localization.SmallShiftedHom W X Y m₀
-- Mathlib.Order.Filter.CountableSeparatingOn
exists_countable_separating : ∀ (α : Type u_1) (p : Set α → Prop) (t : Set α) [h : HasCountableSeparatingOn α p t],
  ∃ S, S.Countable ∧ (∀ s ∈ S, p s) ∧ ∀ x ∈ t, ∀ y ∈ t, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y
-- Mathlib.Tactic.Polynomial.Basic
/-- `polynomial` solves equalities of `Polynomial`s and similar types.

Given a goal which is an equality in `Polynomial R` with a commutative ring `R`, `polynomial`
turns both sides of the equation into a normal form by expanding out the brackets. It then closes
the goal if both sides contain the same terms and fails otherwise. `polynomial_nf` normalizes all
subexpressions at a given location.

Variants of `polynomial` include:
* `polynomial`: normalize both sides of an equation and close the goal if they are equal
* `polynomial!`: run `polynomial` at default transparency
* `polynomial_nf`: normalize all subexpression of the goal
* `polynomial_nf at h₁ h₂ ⊢`: normalize all subexpressions at hypotheses `h₁` `h₁` and the goal
* `polynomial_nf at *`: normalize all subexpressions of all local hypotheses and the goal
* `polynomial_nf!`: run `polynomial_nf` at default transparency

The `polynomial` tactic can be extended to work with algebras other than `Polynomial` using the
attributes `polynomial_infer_base`, `polynomial_pre` and `polynomial_post`. This is only possible
if the base ring can be inferred from the structure of the type.

Examples:

```
example (a : ℚ) : (X + C a) * (X - C a) = X^2 + C (a^2) := by polynomial

example {P : ℚ[X] → Prop} (h : P (X ^ 2 + X + C 4⁻¹)) : P ((X + C 2⁻¹) ^ 2) := by
  polynomial_nf at h ⊢
  exact h
```

 -/
Mathlib.Tactic.Polynomial.polynomial : Lean.ParserDescr
-- Mathlib.Data.NNRat.Defs
NNRat.toNNRat_coe_nat : ∀ (n : ℕ), (↑n).toNNRat = ↑n
-- Init.Data.SInt.Bitwise
ISize.not_neg_one : ~~~(-1) = 0
-- Std.Internal.Do.Order.Basic
/-- The bottom element of the `Prop` lattice is `False`. See `top_prop_eq` for why this is not
`@[simp]`.  -/
Lean.Order.bot_prop_eq : Lean.Order.bot = False
-- Mathlib.Algebra.BigOperators.Group.List.Defs
List.sum_induction_nonempty : ∀ {M : Type u_2} [inst : AddZeroClass M] {l : List M} (p : M → Prop),
  (∀ (a b : M), p a → p b → p (a + b)) → l ≠ [] → (∀ x ∈ l, p x) → p l.sum
-- Mathlib.RingTheory.MvPolynomial.Basic
MvPolynomial.instExpChar : ∀ (σ : Type u) (R : Type v) [inst : CommSemiring R] (p : ℕ) [ExpChar R p], ExpChar (MvPolynomial σ R) p
-- Mathlib.Data.PNat.Xgcd
PNat.XgcdType.step_isSpecial : ∀ (u : PNat.XgcdType), u.IsSpecial → u.step.IsSpecial
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.maxKeyD_insert : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {k : α} {v : β} {fallback : α},
      (t.insert k v).maxKeyD fallback = t.maxKey?.elim k fun k' => if (cmp k' k).isLE = true then k else k'
-- Std.Data.DTreeMap.Raw.Basic
/-- Tries to retrieve the key-value pair with the smallest key that is greater than the given key,
returning `none` if no such pair exists.
 -/
Std.DTreeMap.Raw.getEntryGT? : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → Std.DTreeMap.Raw α β cmp → α → Option ((a : α) × β a)
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F.rightOp : C ⥤ Dᵒᵖ` reflects finite colimits, then `F : Cᵒᵖ ⥤ D` reflects finite
limits.  -/
CategoryTheory.Limits.reflectsFiniteLimits_of_rightOp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor Cᵒᵖ D) [CategoryTheory.Limits.ReflectsFiniteColimits F.rightOp],
  CategoryTheory.Limits.ReflectsFiniteLimits F
-- Mathlib.CategoryTheory.IsConnected
CategoryTheory.IsConnected.prod : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  [CategoryTheory.IsConnected J] [CategoryTheory.IsConnected K], CategoryTheory.IsConnected (J × K)
-- Mathlib.Tactic.GrindAttrs
/-- The `closedness` attribute is a custom grind-set specialized to prove that sets are closed.
It is called by the `closedness` tactic.  -/
Lean.Parser.Attr.closedness! : Lean.ParserDescr
-- Lean.Data.Json.Basic
_private.Lean.Data.Json.Basic.0.Lean.Json.beq' : Lean.Json → Lean.Json → Bool
-- Mathlib.Algebra.Polynomial.Monic
Polynomial.MonicDegreeEq.coeff_of_ge : ∀ {R : Type u} {n : ℕ} [inst : Semiring R] (p : Polynomial.MonicDegreeEq R n) (i : ℕ),
  n ≤ i → (↑p).coeff i = if i = n then 1 else 0
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalSubalgebra.map_injective : ∀ {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : NonUnitalNonAssocSemiring B] [inst_3 : Module R A] [inst_4 : Module R B] [inst_5 : FunLike F A B]
  [inst_6 : NonUnitalAlgHomClass F R A B] {f : F},
  Function.Injective ⇑f → Function.Injective (NonUnitalSubalgebra.map f)
-- Mathlib.RingTheory.Polynomial.Pochhammer
descPochhammer_mul : ∀ (R : Type u) [inst : Ring R] (n m : ℕ),
  descPochhammer R n * (descPochhammer R m).comp (Polynomial.X - ↑n) = descPochhammer R (n + m)
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.norm_eq_sum : ∀ {p : ENNReal} {ι : Type u_2} {β : ι → Type u_4} [inst : Fintype ι] [inst_1 : (i : ι) → Norm (β i)],
  0 < p.toReal → ∀ (f : PiLp p β), ‖f‖ = (∑ i, ‖f.ofLp i‖ ^ p.toReal) ^ (1 / p.toReal)
-- Mathlib.Topology.Algebra.Monoid.Defs
ContinuousWithinAt.const_mul : ∀ {M : Type u_1} [inst : TopologicalSpace M] [inst_1 : Mul M] [SeparatelyContinuousMul M] {X : Type u_2}
  [inst_3 : TopologicalSpace X] {f : X → M} {s : Set X} {x : X},
  ContinuousWithinAt f s x → ∀ (b : M), ContinuousWithinAt (fun x => b * f x) s x
-- Init.Data.String.Decode
_private.Init.Data.String.Decode.0.ByteArray.utf8DecodeChar?.helper₃ : ∀ {x : UInt8},
  ∀ n < 8, (x &&& UInt8.ofNat (2 ^ n - 1)).toUInt32.toBitVec = BitVec.setWidth 32 (BitVec.setWidth n x.toBitVec)
-- Mathlib.RingTheory.Etale.Basic
Algebra.Etale.mk : ∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A],
  autoParam (Algebra.FormallyEtale R A) Algebra.Etale.formallyEtale._autoParam →
    autoParam (Algebra.FinitePresentation R A) Algebra.Etale.finitePresentation._autoParam → Algebra.Etale R A
-- Mathlib.Analysis.Convex.Jensen
/-- A form of the **equality case of Jensen's equality**.

For a strictly concave function `f` and positive weights `w`, if
`f (∑ i ∈ t, w i • p i) = ∑ i ∈ t, w i • f (p i)`, then the points `p` are all equal.

See also `StrictConcaveOn.map_sum_eq_iff`.  -/
StrictConcaveOn.eq_of_map_sum_eq : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} {ι : Type u_5} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜]
  [IsStrictOrderedRing 𝕜] [inst_3 : AddCommGroup E] [inst_4 : AddCommGroup β] [inst_5 : PartialOrder β]
  [IsOrderedAddMonoid β] [inst_7 : Module 𝕜 E] [inst_8 : Module 𝕜 β] [IsStrictOrderedModule 𝕜 β] {s : Set E} {f : E → β}
  {t : Finset ι} {w : ι → 𝕜} {p : ι → E},
  StrictConcaveOn 𝕜 s f →
    (∀ i ∈ t, 0 < w i) →
      ∑ i ∈ t, w i = 1 →
        (∀ i ∈ t, p i ∈ s) →
          f (∑ i ∈ t, w i • p i) ≤ ∑ i ∈ t, w i • f (p i) → ∀ ⦃j : ι⦄, j ∈ t → ∀ ⦃k : ι⦄, k ∈ t → p j = p k
-- Mathlib.CategoryTheory.Limits.Types.Multiequalizer
CategoryTheory.Limits.MulticospanIndex.sections.ext : ∀ {J : CategoryTheory.Limits.MulticospanShape} {I : CategoryTheory.Limits.MulticospanIndex J (Type u)}
  {x y : I.sections}, x.val = y.val → x = y
-- Mathlib.RingTheory.Jacobson.Ideal
Ideal.jacobson_radical_eq_jacobson : ∀ {R : Type u} [inst : CommRing R] {I : Ideal R}, I.radical.jacobson = I.jacobson
-- Batteries.Tactic.Case
/-- Filter the `mvarIds` by tag. Returns those `MVarId`s that have `tag`
either as its user name, as a suffix of its user name, or as a prefix of its user name.
The results are sorted in this order.
This is like `Lean.Elab.Tactic.findTag?` but it returns all results rather than just the first.  -/
_private.Batteries.Tactic.Case.0.Batteries.Tactic.filterTag : List Lean.MVarId → Lean.Name → Lean.Elab.Tactic.TacticM (List Lean.MVarId)
-- Init.Data.Range.Polymorphic.Lemmas
_private.Init.Data.Range.Polymorphic.Lemmas.0.Std.Iter.toArray_eq_match_step.match_1.eq_3 : ∀ {α β : Type u_1} (motive : Std.IterStep (Std.Iter β) β → Sort u_2)
  (h_1 : (it' : Std.Iter β) → (out : β) → motive (Std.IterStep.yield it' out))
  (h_2 : (it' : Std.Iter β) → motive (Std.IterStep.skip it')) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.done with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it' => h_2 it'
    | Std.IterStep.done => h_3 ()) =
    h_3 ()
-- Mathlib.Data.Nat.Fib.Zeckendorf
/-- **Zeckendorf's Theorem** as an equivalence between natural numbers and Zeckendorf
representations. Every natural number can be written uniquely as a sum of non-consecutive Fibonacci
numbers (if we forget about the first two terms `F₀ = 0`, `F₁ = 1`).  -/
Nat.zeckendorfEquiv : ℕ ≃ { l // l.IsZeckendorfRep }
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
ciSup_sup_le : ∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompleteLinearOrder α] {f g : ι → α},
  ⨆ x, max (f x) (g x) ≤ max (⨆ x, f x) (⨆ x, g x)
-- Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling
SimpleGraph.toTopEdgeLabeling_labelGraph_compl : ∀ {V : Type u_1} (G : SimpleGraph V) [inst : DecidableRel G.Adj],
  SimpleGraph.EdgeLabeling.labelGraph G.toTopEdgeLabeling 0 = Gᶜ
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech
CategoryTheory.Limits.FormalCoproduct.cechFunctor_map_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasFiniteProducts C]
  {X Y : CategoryTheory.Limits.FormalCoproduct C} (f : X ⟶ Y) (x : SimplexCategoryᵒᵖ),
  (CategoryTheory.Limits.FormalCoproduct.cechFunctor.map f).app x =
    CategoryTheory.Limits.FormalCoproduct.powerMap f (CategoryTheory.ToType (Opposite.unop x))
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.Multicofork.condition_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape}
  {I : CategoryTheory.Limits.MultispanIndex J C} (K : CategoryTheory.Limits.Multicofork I) (a : J.L) {Z : C}
  (h : K.pt ⟶ Z),
  CategoryTheory.CategoryStruct.comp (I.fst a) (CategoryTheory.CategoryStruct.comp (K.π (J.fst a)) h) =
    CategoryTheory.CategoryStruct.comp (I.snd a) (CategoryTheory.CategoryStruct.comp (K.π (J.snd a)) h)
-- Init.Data.AC
Lean.Data.AC.instReprExpr : Repr Lean.Data.AC.Expr
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.OplaxMonoidal.associativity_assoc : ∀ {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) [self : F.OplaxMonoidal] (X Y Z : C) {Z_1 : D}
  (h :
    CategoryTheory.MonoidalCategoryStruct.tensorObj (F.obj X)
        (CategoryTheory.MonoidalCategoryStruct.tensorObj (F.obj Y) (F.obj Z)) ⟶
      Z_1),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Functor.OplaxMonoidal.δ F (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Functor.OplaxMonoidal.δ F X Y) (F.obj Z))
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).hom h)) =
    CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Functor.OplaxMonoidal.δ F X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z))
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj X) (CategoryTheory.Functor.OplaxMonoidal.δ F Y Z))
          h))
-- Mathlib.CategoryTheory.Category.Basic
/-- Identity morphisms are right identities for composition.  -/
CategoryTheory.Category.comp_id : ∀ {obj : Type u} [self : CategoryTheory.Category.{v, u} obj] {X Y : obj} (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.id Y) = f
-- Mathlib.Tactic.CategoryTheory.Monoidal.Datatypes
Mathlib.Tactic.Monoidal.instMonadCoherehnceHomMonoidalM : Mathlib.Tactic.BicategoryLike.MonadCoherehnceHom Mathlib.Tactic.Monoidal.MonoidalM
-- Init.Internal.Order.Basic
Lean.Order.lfp_fix : ∀ {α : Sort u} [inst : Lean.Order.CompleteLattice α] {f : α → α},
  Lean.Order.monotone f → Lean.Order.lfp f = f (Lean.Order.lfp f)
-- Mathlib.Algebra.Category.Semigrp.Basic
/-- Construct a bundled `MagmaCat` from the underlying type and typeclass.  -/
MagmaCat.of : (M : Type u) → [Mul M] → MagmaCat
-- Mathlib.GroupTheory.GroupAction.Support
MulAction.Supports.mono : ∀ {G : Type u_1} {α : Type u_3} {β : Type u_4} [inst : SMul G α] [inst_1 : SMul G β] {s t : Set α} {b : β},
  s ⊆ t → MulAction.Supports G s b → MulAction.Supports G t b
-- Mathlib.LinearAlgebra.TensorProduct.Vanishing
/-- **Equational criterion for vanishing**
[A. Altman and S. Kleiman, *A term of commutative algebra* (Lemma 8.16)][altman2021term],
generalization.

Assume that the submodule $M' \subseteq M$ generated by the $m_i$ satisfies the
property that the map $M' \otimes N \to M \otimes N$ is injective. Then the expression
$\sum_i m_i \otimes n_i$ vanishes trivially if and only if it vanishes.  -/
TensorProduct.vanishesTrivially_iff_sum_tmul_eq_zero_of_rTensor_injective : ∀ (R : Type u_1) [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {N : Type u_3}
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] {ι : Type u_4} [inst_5 : Fintype ι] {m : ι → M} {n : ι → N},
  Function.Injective ⇑(LinearMap.rTensor N (Submodule.span R (Set.range m)).subtype) →
    (TensorProduct.VanishesTrivially R m n ↔ ∑ i, m i ⊗ₜ[R] n i = 0)
-- Mathlib.Algebra.Group.Pi.Lemmas
/-- **Alias** of `MulHom.pi_injective`. -/
MulHom.injective_pi : ∀ {I : Type u} {f : I → Type v} [inst : (i : I) → Mul (f i)] {γ : Type w} [Nonempty I] [inst_2 : Mul γ]
  (g : (i : I) → γ →ₙ* f i), (∀ (i : I), Function.Injective ⇑(g i)) → Function.Injective ⇑(MulHom.pi g)
-- Mathlib.Algebra.Order.Archimedean.Real.Basic
Real.not_bddAbove_coe : ¬BddAbove (Set.range fun x => ↑x)
-- Init.Data.Int.Gcd
Int.lcm_dvd_lcm_of_dvd_left : ∀ {a b : ℤ} (c : ℤ), a ∣ b → a.lcm c ∣ b.lcm c
-- Mathlib.LinearAlgebra.Complex.Module
skewAdjointPart_eq_I_smul_imaginaryPart : ∀ {A : Type u_1} [inst : AddCommGroup A] [inst_1 : Module ℂ A] [inst_2 : StarAddMonoid A] [inst_3 : StarModule ℂ A]
  (x : A), ↑((skewAdjointPart ℝ) x) = Complex.I • ↑(imaginaryPart x)
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.closure_eq_range : ∀ {β : Type v} [inst : Group β] (s : Set β), Subgroup.closure s = (FreeGroup.lift Subtype.val).range
-- Mathlib.Topology.Instances.Discrete
DiscreteTopology.secondCountableTopology_of_countable : ∀ {α : Type u_1} [inst : TopologicalSpace α] [hd : DiscreteTopology α] [Countable α], SecondCountableTopology α
-- Mathlib.CategoryTheory.Category.PartialFun
PartialFun.instInhabited : Inhabited PartialFun
-- Mathlib.Algebra.Lie.Weights.Basic
/-- If `M` is a representation of a nilpotent Lie algebra `L`, `χ` is a scalar, and `x : L`, then
`genWeightSpaceOf M χ x` is the maximal generalized `χ`-eigenspace of the action of `x` on `M`.

It is a Lie submodule because `L` is nilpotent.  -/
LieModule.genWeightSpaceOf : {R : Type u_2} →
  {L : Type u_3} →
    (M : Type u_4) →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [inst_2 : LieAlgebra R L] →
            [inst_3 : AddCommGroup M] →
              [inst_4 : Module R M] →
                [inst_5 : LieRingModule L M] → [LieModule R L M] → [LieRing.IsNilpotent L] → R → L → LieSubmodule R L M
-- Mathlib.CategoryTheory.Products.Associator
CategoryTheory.prod.associativity_functor : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (E : Type u₃) [inst_2 : CategoryTheory.Category.{v₃, u₃} E],
  (CategoryTheory.prod.associativity C D E).functor = CategoryTheory.prod.associator C D E
-- Mathlib.Analysis.Calculus.FDeriv.Prod
HasStrictFDerivAt.finCons : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : E} {n : ℕ} {F' : Fin n.succ → Type u_6}
  [inst_3 : (i : Fin n.succ) → NormedAddCommGroup (F' i)] [inst_4 : (i : Fin n.succ) → NormedSpace 𝕜 (F' i)]
  {φ : E → F' 0} {φs : E → (i : Fin n) → F' i.succ} {φ' : E →L[𝕜] F' 0} {φs' : E →L[𝕜] (i : Fin n) → F' i.succ},
  HasStrictFDerivAt φ φ' x →
    HasStrictFDerivAt φs φs' x → HasStrictFDerivAt (fun x => Fin.cons (φ x) (φs x)) (φ'.finCons φs') x
-- Mathlib.MeasureTheory.Measure.Lebesgue.Basic
regionBetween.eq_1 : ∀ {α : Type u_1} (f g : α → ℝ) (s : Set α), regionBetween f g s = {p | p.1 ∈ s ∧ p.2 ∈ Set.Ioo (f p.1) (g p.1)}
-- Mathlib.Data.Finsupp.Multiset
Finsupp.toMultiset_zero : ∀ {α : Type u_1}, Finsupp.toMultiset 0 = 0
-- Mathlib.RingTheory.Ideal.Span
Ideal.span_eq : ∀ {α : Type u} [inst : Semiring α] (I : Ideal α), Ideal.span ↑I = I
-- Mathlib.Topology.VectorBundle.Basic
/-- The zero section of a vector bundle is continuous on any set.  -/
Bundle.Trivialization.continuousOn_zeroSection : ∀ (R : Type u_1) {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [inst : NontriviallyNormedField R]
  [inst_1 : (x : B) → AddCommMonoid (E x)] [inst_2 : (x : B) → Module R (E x)] [inst_3 : NormedAddCommGroup F]
  [inst_4 : NormedSpace R F] [inst_5 : TopologicalSpace B] [inst_6 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_7 : (x : B) → TopologicalSpace (E x)] [inst_8 : FiberBundle F E] [VectorBundle R F E] (s : Set B),
  ContinuousOn (Bundle.zeroSection F E) s
-- Mathlib.MeasureTheory.Measure.Stieltjes
StieltjesFunction.isProbabilityMeasure : ∀ {R : Type u_1} [inst : LinearOrder R] [inst_1 : TopologicalSpace R] (f : StieltjesFunction R)
  [inst_2 : OrderTopology R] [inst_3 : CompactIccSpace R] [inst_4 : MeasurableSpace R] [inst_5 : BorelSpace R]
  [inst_6 : SecondCountableTopology R] [inst_7 : DenselyOrdered R] [Nonempty R],
  Filter.Tendsto (↑f) Filter.atBot (nhds 0) →
    Filter.Tendsto (↑f) Filter.atTop (nhds 1) → MeasureTheory.IsProbabilityMeasure f.measure
-- Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
/-- If an affine independent finset is contained in the affine span of another finset, then its
cardinality is at most the cardinality of that finset.  -/
AffineIndependent.card_le_card_of_subset_affineSpan : ∀ {k : Type u_1} {V : Type u_2} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  {s t : Finset V}, AffineIndependent k Subtype.val → ↑s ⊆ ↑(affineSpan k ↑t) → s.card ≤ t.card
-- Aesop.Tree.Data
Aesop.GoalUnsafe.brecOn_1.eq : ∀ {motive_1 : Aesop.GoalUnsafe → Sort u} {motive_2 : Aesop.MVarClusterUnsafe → Sort u}
  {motive_3 : Aesop.RappUnsafe → Sort u} {motive_4 : Aesop.GoalData Aesop.RappUnsafe Aesop.MVarClusterUnsafe → Sort u}
  {motive_5 : Aesop.MVarClusterData Aesop.GoalUnsafe Aesop.RappUnsafe → Sort u}
  {motive_6 : Aesop.RappData Aesop.GoalUnsafe Aesop.MVarClusterUnsafe → Sort u}
  {motive_7 : Array (IO.Ref Aesop.RappUnsafe) → Sort u} {motive_8 : Option (IO.Ref Aesop.RappUnsafe) → Sort u}
  {motive_9 : Array (IO.Ref Aesop.GoalUnsafe) → Sort u} {motive_10 : Array (IO.Ref Aesop.MVarClusterUnsafe) → Sort u}
  {motive_11 : List (IO.Ref Aesop.RappUnsafe) → Sort u} {motive_12 : List (IO.Ref Aesop.GoalUnsafe) → Sort u}
  {motive_13 : List (IO.Ref Aesop.MVarClusterUnsafe) → Sort u}
  (t : Aesop.GoalData Aesop.RappUnsafe Aesop.MVarClusterUnsafe) (F_1 : (t : Aesop.GoalUnsafe) → t.below → motive_1 t)
  (F_2 : (t : Aesop.MVarClusterUnsafe) → t.below → motive_2 t) (F_3 : (t : Aesop.RappUnsafe) → t.below → motive_3 t)
  (F_4 : (t : Aesop.GoalData Aesop.RappUnsafe Aesop.MVarClusterUnsafe) → Aesop.GoalUnsafe.below_1 t → motive_4 t)
  (F_5 : (t : Aesop.MVarClusterData Aesop.GoalUnsafe Aesop.RappUnsafe) → Aesop.GoalUnsafe.below_2 t → motive_5 t)
  (F_6 : (t : Aesop.RappData Aesop.GoalUnsafe Aesop.MVarClusterUnsafe) → Aesop.GoalUnsafe.below_3 t → motive_6 t)
  (F_7 : (t : Array (IO.Ref Aesop.RappUnsafe)) → Aesop.GoalUnsafe.below_4 t → motive_7 t)
  (F_8 : (t : Option (IO.Ref Aesop.RappUnsafe)) → Aesop.GoalUnsafe.below_5 t → motive_8 t)
  (F_9 : (t : Array (IO.Ref Aesop.GoalUnsafe)) → Aesop.GoalUnsafe.below_6 t → motive_9 t)
  (F_10 : (t : Array (IO.Ref Aesop.MVarClusterUnsafe)) → Aesop.GoalUnsafe.below_7 t → motive_10 t)
  (F_11 : (t : List (IO.Ref Aesop.RappUnsafe)) → Aesop.GoalUnsafe.below_8 t → motive_11 t)
  (F_12 : (t : List (IO.Ref Aesop.GoalUnsafe)) → Aesop.GoalUnsafe.below_9 t → motive_12 t)
  (F_13 : (t : List (IO.Ref Aesop.MVarClusterUnsafe)) → Aesop.GoalUnsafe.below_10 t → motive_13 t),
  Aesop.GoalUnsafe.brecOn_1 t F_1 F_2 F_3 F_4 F_5 F_6 F_7 F_8 F_9 F_10 F_11 F_12 F_13 =
    F_4 t (Aesop.GoalUnsafe.brecOn_1.go t F_1 F_2 F_3 F_4 F_5 F_6 F_7 F_8 F_9 F_10 F_11 F_12 F_13).2
-- Mathlib.Algebra.Homology.HomologySequence
/-- Exactness of `S.X₁.homology i ⟶ S.X₂.homology i ⟶ S.X₃.homology i`.  -/
CategoryTheory.ShortComplex.ShortExact.homology_exact₂ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {c : ComplexShape ι} {S : CategoryTheory.ShortComplex (HomologicalComplex C c)},
  S.ShortExact →
    ∀ (i : ι),
      { X₁ := S.X₁.homology i, X₂ := S.X₂.homology i, X₃ := S.X₃.homology i, f := HomologicalComplex.homologyMap S.f i,
          g := HomologicalComplex.homologyMap S.g i, zero := ⋯ }.Exact
-- Mathlib.CategoryTheory.Limits.Connected
CategoryTheory.Limits.Cone.isLimit_iff_isIso_limMap_π : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} C]
  [inst_2 : CategoryTheory.IsConnected J] {F : CategoryTheory.Functor J C} [inst_3 : CategoryTheory.Limits.HasLimit F]
  (c : CategoryTheory.Limits.Cone F),
  Nonempty (CategoryTheory.Limits.IsLimit c) ↔ CategoryTheory.IsIso (CategoryTheory.Limits.limMap c.π)
-- Mathlib.GroupTheory.Sylow
Sylow.ne_bot_of_dvd_card : ∀ {G : Type u} [inst : Group G] [Finite G] {p : ℕ} [hp : Fact (Nat.Prime p)] (P : Sylow p G), p ∣ Nat.card G → ↑P ≠ ⊥
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
ENNReal.rpow_add : ∀ {x : ENNReal} (y z : ℝ), x ≠ 0 → x ≠ ⊤ → x ^ (y + z) = x ^ y * x ^ z
-- Mathlib.Order.LiminfLimsup
Filter.blimsup_eq_iInf_biSup : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {f : Filter β} {p : β → Prop} {u : β → α},
  Filter.blimsup u f p = ⨅ s ∈ f, ⨆ b, ⨆ (_ : p b ∧ b ∈ s), u b
-- Init.Data.Queue
Std.Queue.instEmptyCollection : {α : Type u} → EmptyCollection (Std.Queue α)
-- Mathlib.Algebra.Order.Nonneg.Ring
Nonneg.linearOrderedCommMonoidWithZero : {α : Type u_1} →
  [inst : CommSemiring α] →
    [inst_1 : LinearOrder α] → [IsStrictOrderedRing α] → LinearOrderedCommMonoidWithZero { x // 0 ≤ x }
-- Mathlib.Topology.Hom.Open
ContinuousOpenMap.toFun_eq_coe : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α →CO β}, f.toFun = ⇑f
-- Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
Subgroup.instEncodableSubtypeMulOppositeMemOp : {G : Type u_2} → [inst : Group G] → (H : Subgroup G) → [Encodable ↥H] → Encodable ↥H.op
-- Mathlib.MeasureTheory.Integral.Bochner.L1
MeasureTheory.L1.integral_eq_norm_posPart_sub : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (f : ↥(MeasureTheory.Lp ℝ 1 μ)),
  MeasureTheory.L1.integral f = ‖MeasureTheory.Lp.posPart f‖ - ‖MeasureTheory.Lp.negPart f‖