mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
/-- A functor `F : C ⥤ D` reflects colimits of shape `J` if
whenever the image of a cocone over some `K : J ⥤ C` under `F` is a colimit cocone in `D`,
the cocone was already a colimit cocone in `C`.
Note that we do not assume a priori that `D` actually has any colimits.
 -/
CategoryTheory.Limits.ReflectsColimitsOfShape : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (J : Type w) → [CategoryTheory.Category.{w', w} J] → CategoryTheory.Functor C D → Prop
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
CategoryTheory.Limits.PullbackCone.IsLimit.hom_ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z}
  {t : CategoryTheory.Limits.PullbackCone f g} (ht : CategoryTheory.Limits.IsLimit t) {W : C} {k l : W ⟶ t.pt},
  CategoryTheory.CategoryStruct.comp k t.fst = CategoryTheory.CategoryStruct.comp l t.fst →
    CategoryTheory.CategoryStruct.comp k t.snd = CategoryTheory.CategoryStruct.comp l t.snd → k = l
-- Mathlib.Algebra.Lie.Character
LieAlgebra.lieCharacterEquivLinearDual_symm_apply : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] [inst_3 : IsLieAbelian L]
  (ψ : Module.Dual R L), LieAlgebra.lieCharacterEquivLinearDual.symm ψ = { toLinearMap := ψ, map_lie' := ⋯ }
-- Mathlib.Geometry.Manifold.ChartedSpace
chart_mem_atlas : ∀ (H : Type u_5) {M : Type u_6} [inst : TopologicalSpace H] [inst_1 : TopologicalSpace M] [inst_2 : ChartedSpace H M]
  (x : M), chartAt H x ∈ atlas H M
-- Std.Internal.Parsec.Basic
Std.Internal.Parsec.instReprParseResult : {α ι : Type} → [Repr α] → [Repr ι] → Repr (Std.Internal.Parsec.ParseResult α ι)
-- Mathlib.Logic.Basic
/-- Provide the reverse of modus tollens (`mt`) as dot notation for implications.  -/
Function.mtr : ∀ {a b : Prop}, (¬a → ¬b) → b → a
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.equivFunOnFintype_symm_coe : ∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → Zero (β i)] [inst_1 : Fintype ι] (f : Π₀ (i : ι), β i),
  DFinsupp.equivFunOnFintype.symm ⇑f = f
-- Mathlib.Algebra.Group.ModEq
AddCommGroup.nsmul_add_modEq : ∀ {M : Type u_1} [inst : AddCommMonoid M] {a p : M} (n : ℕ), n • p + a ≡ a [PMOD p]
-- Mathlib.Combinatorics.SimpleGraph.Copy
/-- An injective homomorphism gives rise to a copy.  -/
SimpleGraph.Hom.toCopy : {α : Type u_4} →
  {β : Type u_5} → {A : SimpleGraph α} → {B : SimpleGraph β} → (f : A →g B) → Function.Injective ⇑f → A.Copy B
-- Init.Data.List.Monadic
List.forIn'_pure_yield_eq_foldl : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] [LawfulMonad m] {l : List α}
  (f : (a : α) → a ∈ l → β → β) (init : β),
  (forIn' l init fun a m_1 b => pure (ForInStep.yield (f a m_1 b))) =
    pure
      (List.foldl
        (fun b x =>
          match x with
          | ⟨a, h⟩ => f a h b)
        init l.attach)
-- Mathlib.MeasureTheory.Function.LocallyIntegrable
/-- A function `f : X → ε` is *locally integrable* if it is integrable on a neighborhood of every
point. In particular, it is integrable on all compact sets,
see `LocallyIntegrable.integrableOn_isCompact`.  -/
MeasureTheory.LocallyIntegrable : {X : Type u_1} →
  {ε : Type u_3} →
    [inst : MeasurableSpace X] →
      [TopologicalSpace X] →
        [inst_2 : TopologicalSpace ε] →
          [ContinuousENorm ε] →
            (X → ε) → autoParam (MeasureTheory.Measure X) MeasureTheory.LocallyIntegrable._auto_1 → Prop
-- Mathlib.Algebra.Lie.Normalizer
LieSubalgebra.mem_normalizer_iff' : ∀ {R : Type u_1} {L : Type u_2} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  (H : LieSubalgebra R L) (x : L), x ∈ H.normalizer ↔ ∀ y ∈ H, ⁅y, x⁆ ∈ H
-- Mathlib.RingTheory.Algebraic.Basic
IsAlgebraic.nontrivial : ∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] {a : A},
  IsAlgebraic R a → Nontrivial R
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F.op : Cᵒᵖ ⥤ Dᵒᵖ` preserves finite colimits, then `F : C ⥤ D` preserves finite limits.  -/
CategoryTheory.Limits.preservesFiniteLimits_of_op : ∀ {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.PreservesFiniteColimits F.op],
  CategoryTheory.Limits.PreservesFiniteLimits F
-- Mathlib.RingTheory.Localization.AtPrime.Extension
IsLocalization.AtPrime.inertiaDeg_map_eq_inertiaDeg : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal R)
  [inst_3 : p.IsPrime] (Rₚ : Type u_3) [inst_4 : CommRing Rₚ] [inst_5 : Algebra R Rₚ] [IsLocalization.AtPrime Rₚ p]
  [inst_7 : IsLocalRing Rₚ] (Sₚ : Type u_4) [inst_8 : CommRing Sₚ] [inst_9 : Algebra S Sₚ]
  [IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ] [inst_11 : Algebra Rₚ Sₚ] (P : Ideal S)
  [hPp : P.LiesOver p] [inst_12 : Algebra R Sₚ] [IsScalarTower R S Sₚ] [IsScalarTower R Rₚ Sₚ] [p.IsMaximal]
  [P.IsMaximal] [(Ideal.map (algebraMap S Sₚ) P).LiesOver (IsLocalRing.maximalIdeal Rₚ)],
  (IsLocalRing.maximalIdeal Rₚ).inertiaDeg' (Ideal.map (algebraMap S Sₚ) P) = p.inertiaDeg' P
-- Mathlib.Analysis.Real.Cardinality
/-- The cardinality of the reals, as a set.  -/
Cardinal.mk_univ_real : Cardinal.mk ↑Set.univ = Cardinal.continuum
-- Mathlib.Algebra.LieRinehartAlgebra.Defs
/-- A Lie-Rinehart algebra with coefficients in a commutative ring `R`, is a pair consisting of a
commutative `R`-algebra `A` and a Lie algebra `L` with coefficients in `R`, such that `A` and `L`
are each a module over the other, satisfying compatibility conditions.

As shown below, this data determines a linear map `L → Derivation R A A` satisfying a Leibniz-like
compatibility condition. This could even be taken as a definition, however the definition here has
the advantage of being `Prop`-valued, thus mitigating potential diamonds.  -/
LieRinehartAlgebra : (R : Type u_1) →
  (A : Type u_2) →
    (L : Type u_3) →
      [inst : CommRing A] →
        [inst_1 : LieRing L] →
          [inst_2 : Module A L] →
            [inst_3 : LieRingModule L A] →
              [LieRinehartRing A L] → [inst_5 : CommRing R] → [Algebra R A] → [LieAlgebra R L] → Prop
-- Mathlib.Order.BooleanAlgebra.Basic
sdiff_right_inj : ∀ {α : Type u} {x y z : α} [inst : GeneralizedBooleanAlgebra α], x ≤ z → y ≤ z → (z \ x = z \ y ↔ x = y)
-- Mathlib.MeasureTheory.Integral.Average
/-- Average value of a function `f` w.r.t. a measure `μ`, denoted `⨍ x, f x ∂μ`.

It is equal to `(μ.real univ)⁻¹ • ∫ x, f x ∂μ`, so it takes value zero if `f` is not integrable or
if `μ` is an infinite measure. If `μ` is a probability measure, then the average of any function is
equal to its integral.

For the average on a set, use `⨍ x in s, f x ∂μ`, defined as `⨍ x, f x ∂(μ.restrict s)`. For the
average w.r.t. the volume, one can omit `∂volume`.  -/
MeasureTheory.average : {α : Type u_1} →
  {E : Type u_2} →
    {m0 : MeasurableSpace α} → [inst : NormedAddCommGroup E] → [NormedSpace ℝ E] → MeasureTheory.Measure α → (α → E) → E
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPowerSeries.X_dvd_iff : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] {s : σ} {φ : MvPowerSeries σ R},
  MvPowerSeries.X s ∣ φ ↔ ∀ (m : σ →₀ ℕ), m s = 0 → (MvPowerSeries.coeff m) φ = 0
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
/-- **Fundamental theorem of calculus-1**: if `f : ℝ → E` is integrable on `a..b` and `f x` has a
finite limit `c` almost surely at `b`, then `u ↦ ∫ x in a..u, f x` has derivative `c` at `b`.  -/
intervalIntegral.integral_hasDerivAt_of_tendsto_ae_right : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E} {c : E}
  {a b : ℝ},
  IntervalIntegrable f MeasureTheory.volume a b →
    StronglyMeasurableAtFilter f (nhds b) MeasureTheory.volume →
      Filter.Tendsto f (nhds b ⊓ MeasureTheory.ae MeasureTheory.volume) (nhds c) →
        HasDerivAt (fun u => ∫ (x : ℝ) in a..u, f x) c b
-- Mathlib.CategoryTheory.Generator.Preadditive
CategoryTheory.Preadditive.isSeparator_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] (G : C),
  CategoryTheory.IsSeparator G ↔
    ∀ ⦃X Y : C⦄ (f : X ⟶ Y), (∀ (h : G ⟶ X), CategoryTheory.CategoryStruct.comp h f = 0) → f = 0
-- Mathlib.Algebra.Module.Submodule.Range
LinearMap.range_eq_top_of_surjective : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  [inst_6 : RingHomSurjective τ₁₂] (f : M →ₛₗ[τ₁₂] M₂), Function.Surjective ⇑f → f.range = ⊤
-- Mathlib.Analysis.Analytic.Constructions
/-- Eta-expanded form of `AnalyticAt.pow`

---

Powers of analytic functions (into a normed `𝕜`-algebra) are analytic.  -/
AnalyticAt.fun_pow : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {A : Type u_7} [inst_3 : NormedRing A] [inst_4 : NormedAlgebra 𝕜 A] {f : E → A} {z : E},
  AnalyticAt 𝕜 f z → ∀ (n : ℕ), AnalyticAt 𝕜 (fun i => f i ^ n) z
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.sum_excenterWeights : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex ℝ P n) (signs : Finset (Fin (n + 1)))
  [inst_5 : Decidable (s.ExcenterExists signs)],
  ∑ i, s.excenterWeights signs i = if s.ExcenterExists signs then 1 else 0
-- Mathlib.RingTheory.TensorProduct.IsBaseChangePi
/-- Base change for direct sums of a constant module.  -/
IsBaseChange.directSumPow : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (ι : Type u_3)
  {M : Type u_6} {M' : Type u_7} [inst_3 : AddCommMonoid M] [inst_4 : AddCommMonoid M'] [inst_5 : Module R M]
  [inst_6 : Module R M'] [inst_7 : Module S M'] [inst_8 : IsScalarTower R S M'] {ε : M →ₗ[R] M'},
  IsBaseChange S ε → IsBaseChange S (DirectSum.lmap fun x => ε)
-- Init.Data.List.Lemmas
List.insert_replicate_self : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {n : ℕ} {a : α},
  0 < n → List.insert a (List.replicate n a) = List.replicate n a
-- Mathlib.NumberTheory.SumPrimeReciprocals
_private.Mathlib.NumberTheory.SumPrimeReciprocals.0.ite_prime_eq_mulIndicator : ∀ {M : Type u_1} [inst : CommMonoid M] (f : ℕ → M),
  (fun n => if Nat.Prime n then f n else 1) = {n | Nat.Prime n}.mulIndicator f
-- Mathlib.Analysis.Calculus.Deriv.Polynomial
/-- The derivative (in the analysis sense) of a polynomial `p` is given by `p.derivative`.  -/
Polynomial.hasStrictDerivAt : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] (p : Polynomial 𝕜) (x : 𝕜),
  HasStrictDerivAt (fun x => Polynomial.eval x p) (Polynomial.eval x (Polynomial.derivative p)) x
-- Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset
PartOrdEmb.isCardinalFiltered_iff : ∀ (κ : Cardinal.{u}) [inst : Fact κ.IsRegular] (X : PartOrdEmb),
  PartOrdEmb.isCardinalFiltered κ X ↔ CategoryTheory.IsCardinalFiltered (↑X) κ
-- Mathlib.Probability.Independence.Conditional
ProbabilityTheory.condIndepFun_iff_condExp_inter_preimage_eq_mul : ∀ {Ω : Type u_1} {β : Type u_3} {β' : Type u_4} {m' mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω]
  {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [inst_1 : MeasureTheory.IsFiniteMeasure μ] {f : Ω → β} {g : Ω → β'}
  {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'},
  Measurable f →
    Measurable g →
      (ProbabilityTheory.CondIndepFun m' hm' f g μ ↔
        ∀ (s : Set β) (t : Set β'),
          MeasurableSet s →
            MeasurableSet t →
              μ[(f ⁻¹' s ∩ g ⁻¹' t).indicator fun ω => 1 | m'] =ᵐ[μ] fun ω =>
                μ[(f ⁻¹' s).indicator fun ω => 1 | m'] ω * μ[(g ⁻¹' t).indicator fun ω => 1 | m'] ω)
-- Mathlib.CategoryTheory.Monoidal.Bimon_
CategoryTheory.Bimon.instBimonObjXXMon : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] → (M : CategoryTheory.Bimon C) → CategoryTheory.BimonObj M.X.X
-- Mathlib.NumberTheory.Padics.PadicVal.Basic
/-- **Kummer's Theorem**
Taking (`p - 1`) times the `p`-adic valuation of the binomial `n + k` over `k` equals the sum of the
digits of `k` plus the sum of the digits of `n` minus the sum of digits of `n + k`, all base `p`.
 -/
sub_one_mul_padicValNat_choose_eq_sub_sum_digits' : ∀ {p k n : ℕ} [hp : Fact (Nat.Prime p)],
  (p - 1) * padicValNat p ((n + k).choose k) = (p.digits k).sum + (p.digits n).sum - (p.digits (n + k)).sum
-- Mathlib.CategoryTheory.Shift.SingleFunctorsLift
CategoryTheory.SingleFunctors.map_lift_shiftIso_hom_app : ∀ {C : Type u_1} {D : Type u_2} {E : Type u_3} [inst : CategoryTheory.Category.{u_7, u_1} C]
  [inst_1 : CategoryTheory.Category.{u_6, u_2} D] [inst_2 : CategoryTheory.Category.{u_5, u_3} E] {A : Type u_4}
  [inst_3 : AddMonoid A] [inst_4 : CategoryTheory.HasShift D A] [inst_5 : CategoryTheory.HasShift E A]
  (F : CategoryTheory.SingleFunctors C E A) (G : CategoryTheory.Functor D E) [inst_6 : G.CommShift A] [inst_7 : G.Full]
  [inst_8 : G.Faithful] (Φ : A → CategoryTheory.Functor C D) (hΦ : (a : A) → (Φ a).comp G ≅ F.functor a) (n a a' : A)
  (h : n + a = a') (X : C),
  G.map (((F.lift G Φ hΦ).shiftIso n a a' h).hom.app X) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.commShiftIso G n).hom.app ((Φ a').obj X))
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor E n).map ((hΦ a').hom.app X))
        (CategoryTheory.CategoryStruct.comp ((F.shiftIso n a a' h).hom.app X) ((hΦ a).inv.app X)))
-- Init.Data.Subtype.Order
Subtype.instTotalLE : ∀ {α : Type u} [inst : LE α] [i : Std.Total fun x1 x2 => x1 ≤ x2] {P : α → Prop}, Std.Total fun x1 x2 => x1 ≤ x2
-- Mathlib.Analysis.InnerProductSpace.Dual
InnerProductSpace.toDual_apply_eq_toDualMap_apply : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : CompleteSpace E] (x : E), (InnerProductSpace.toDual 𝕜 E) x = (InnerProductSpace.toDualMap 𝕜 E) x
-- Mathlib.Combinatorics.SimpleGraph.Copy
/-- A `Subgraph G` gives rise to a copy from the coercion to `G`.  -/
SimpleGraph.Subgraph.coeCopy : {V : Type u_1} → {G : SimpleGraph V} → (G' : G.Subgraph) → G'.coe.Copy G
-- Mathlib.Topology.DiscreteQuotient
/-- The discrete quotients of a compact space are in bijection with a subtype of the type of
`Finset (Clopens X)`.

TODO: show that this is precisely those finsets of clopens which form a partition of `X`.
 -/
DiscreteQuotient.equivFinsetClopens : (X : Type u_2) →
  [inst : TopologicalSpace X] →
    [inst_1 : CompactSpace X] → DiscreteQuotient X ≃ ↑(Set.range (DiscreteQuotient.finsetClopens X))
-- Mathlib.Control.ULiftable
/-- A version of `up` for a `PUnit` return type.  -/
ULiftable.up' : {f : Type u₀ → Type u₁} → {g : Type v₀ → Type v₁} → [ULiftable f g] → f PUnit.{u₀ + 1} → g PUnit.{v₀ + 1}
-- Mathlib.Combinatorics.SimpleGraph.Finite
SimpleGraph.map_neighborFinset_induce_of_neighborSet_subset : ∀ {V : Type u_1} {s : Set V} [inst : DecidablePred fun x => x ∈ s] [inst_1 : Fintype V] {G : SimpleGraph V}
  [inst_2 : DecidableRel G.Adj] {v : ↑s},
  G.neighborSet ↑v ⊆ s →
    Finset.map (Function.Embedding.subtype fun x => x ∈ s) ((SimpleGraph.induce s G).neighborFinset v) =
      G.neighborFinset ↑v
-- Init.Data.List.Attach
List.pmap_attach : ∀ {α : Type u_1} {β : Type u_2} {l : List α} {p : { x // x ∈ l } → Prop} {f : (a : { x // x ∈ l }) → p a → β}
  (H : ∀ a ∈ l.attach, p a), List.pmap f l.attach H = List.pmap (fun a h => f ⟨a, ⋯⟩ ⋯) l ⋯
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.inv_hom_h₁_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E F : CategoryTheory.PreOneHypercover S} (e : E ≅ F)
  {i j : F.I₀} (k : F.I₁ i j) {Z : C} (h : F.Y (e.hom.s₁ (e.inv.s₁ k)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (e.inv.h₁ k) (CategoryTheory.CategoryStruct.comp (e.hom.h₁ (e.inv.s₁ k)) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.PreOneHypercover.congrIndexOneOfEqIso ⋯ ⋯ k).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) h)
-- Mathlib.Algebra.Polynomial.EraseLead
Polynomial.eraseLead_monomial : ∀ {R : Type u_1} [inst : Semiring R] (i : ℕ) (r : R), ((Polynomial.monomial i) r).eraseLead = 0
-- Mathlib.Algebra.Group.Opposite
AddSemiconjBy.unop : ∀ {α : Type u_1} [inst : Add α] {a x y : αᵃᵒᵖ},
  AddSemiconjBy a x y → AddSemiconjBy (AddOpposite.unop a) (AddOpposite.unop y) (AddOpposite.unop x)
-- Mathlib.Logic.Equiv.Sum
Equiv.sigmaSumDistrib_apply : ∀ {ι : Type u_11} (α : ι → Type u_9) (β : ι → Type u_10) (p : (i : ι) × (α i ⊕ β i)),
  (Equiv.sigmaSumDistrib α β) p = Sum.map (Sigma.mk p.fst) (Sigma.mk p.fst) p.snd
-- Mathlib.Algebra.Order.Archimedean.Real.Hom
/-- There exists no nontrivial ring homomorphism `ℝ →+* ℝ`.  -/
Real.RingHom.unique : Unique (ℝ →+* ℝ)
-- Mathlib.Data.Num.ZNum
Num.mod.eq_3 : ∀ (a b : PosNum), (Num.pos a).mod (Num.pos b) = a.mod' b
-- Mathlib.Topology.MetricSpace.Bounded
Metric.exists_isBounded_image_of_tendsto : ∀ {α : Type u_3} {β : Type u_4} [inst : PseudoMetricSpace β] {l : Filter α} {f : α → β} {x : β},
  Filter.Tendsto f l (nhds x) → ∃ s ∈ l, Bornology.IsBounded (f '' s)
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.prod.map_mono : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W X Y Z : C} (f : W ⟶ Y) (g : X ⟶ Z)
  [CategoryTheory.Mono f] [CategoryTheory.Mono g] [inst_3 : CategoryTheory.Limits.HasBinaryProduct W X]
  [inst_4 : CategoryTheory.Limits.HasBinaryProduct Y Z], CategoryTheory.Mono (CategoryTheory.Limits.prod.map f g)
-- Init.Data.Iterators.Lemmas.Producers.List
List.step_iter_cons : ∀ {β : Type w} {x : β} {xs : List β}, (x :: xs).iter.step = ⟨Std.IterStep.yield xs.iter x, ⋯⟩
-- Mathlib.Algebra.Lie.Rank
LieModule.rank_le_finrank : ∀ (R : Type u_1) (L : Type u_3) (M : Type u_4) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : Module.Finite R L] [inst_4 : Module.Free R L] [inst_5 : AddCommGroup M] [inst_6 : Module R M]
  [inst_7 : LieRingModule L M] [inst_8 : LieModule R L M] [inst_9 : Module.Finite R M] [inst_10 : Module.Free R M]
  [Nontrivial R], LieModule.rank R L M ≤ Module.finrank R M
-- Init.WFTactics
/-- Unfold definitions commonly used in well founded relation definitions.

Since Lean 4.12, Lean unfolds these definitions automatically before presenting the goal to the
user, and this tactic should no longer be necessary. Calls to `simp_wf` can be removed or replaced
by plain calls to `simp`.
 -/
tacticSimp_wf : Lean.ParserDescr
-- Mathlib.Topology.Separation.GDelta
Set.Finite.isGδ_compl : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X} [T1Space X], s.Finite → IsGδ sᶜ
-- Mathlib.Algebra.Lie.Classical
/-- The classical Lie algebra of type B as a Lie subalgebra of matrices associated to the matrix
`JB`.  -/
LieAlgebra.Orthogonal.typeB : (l : Type u_4) →
  (R : Type u₂) →
    [inst : DecidableEq l] →
      [inst_1 : CommRing R] → [inst_2 : Fintype l] → LieSubalgebra R (Matrix (Unit ⊕ l ⊕ l) (Unit ⊕ l ⊕ l) R)
-- Batteries.Data.Array.Match
/-- Transition function for the KMP matcher

Assuming we have an input `xs` with a suffix that matches the pattern prefix `t.pattern[:len]`
where `len : Fin (t.size+1)`. Then `xs.push x` has a suffix that matches the pattern prefix
`t.pattern[:t.step x len]`. If `len` is as large as possible then `t.step x len` will also be
as large as possible.
 -/
Array.PrefixTable.step : {α : Type u_1} → [BEq α] → (t : Array.PrefixTable α) → α → Fin (t.size + 1) → Fin (t.size + 1)
-- Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
/-- A functor that preserves initial objects and pushouts preserves binary coproducts.  -/
preservesBinaryCoproducts_of_preservesInitial_and_pushouts : ∀ {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.HasInitial C] [CategoryTheory.Limits.HasPushouts C]
  [CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) F]
  [CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingSpan F],
  CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F
-- Mathlib.Data.Finset.Sigma
/-- Lifts maps `α i → β i → Finset (γ i)` to a map `Σ i, α i → Σ i, β i → Finset (Σ i, γ i)`.  -/
Finset.sigmaLift : {ι : Type u_1} →
  {α : ι → Type u_2} →
    {β : ι → Type u_3} →
      {γ : ι → Type u_4} → [DecidableEq ι] → (⦃i : ι⦄ → α i → β i → Finset (γ i)) → Sigma α → Sigma β → Finset (Sigma γ)
-- Mathlib.CategoryTheory.Monoidal.ExternalProduct.Basic
CategoryTheory.MonoidalCategory.externalProductBifunctorCurried_obj_map_app_app : ∀ (J₁ : Type u₁) (J₂ : Type u₂) (C : Type u₃) [inst : CategoryTheory.Category.{v₁, u₁} J₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} J₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  [inst_3 : CategoryTheory.MonoidalCategory C] (X : CategoryTheory.Functor J₁ C) {X_1 Y : CategoryTheory.Functor J₂ C}
  (f : X_1 ⟶ Y) (X_2 : J₁) (c : J₂),
  ((((CategoryTheory.MonoidalCategory.externalProductBifunctorCurried J₁ J₂ C).obj X).map f).app X_2).app c =
    CategoryTheory.MonoidalCategoryStruct.whiskerLeft (X.obj X_2) (f.app c)
-- Mathlib.MeasureTheory.Measure.Real
MeasureTheory.measureReal_union_null : ∀ {α : Type u_1} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s₁ s₂ : Set α},
  μ.real s₁ = 0 → μ.real s₂ = 0 → μ.real (s₁ ∪ s₂) = 0
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.Equiv.minEntry?_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.minEntry? = t₂.minEntry?
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.C_mul_X_pow_eq_monomial : ∀ {R : Type u} {a : R} [inst : Semiring R] {n : ℕ}, Polynomial.C a * Polynomial.X ^ n = (Polynomial.monomial n) a
-- Mathlib.MeasureTheory.Integral.Lebesgue.Add
/-- **Fatou's lemma**, version with `AEMeasurable` functions.  -/
MeasureTheory.lintegral_liminf_le' : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ι : Type u_3} {f : ι → α → ENNReal}
  {u : Filter ι} [u.IsCountablyGenerated],
  (∀ (i : ι), AEMeasurable (f i) μ) →
    ∫⁻ (a : α), Filter.liminf (fun i => f i a) u ∂μ ≤ Filter.liminf (fun i => ∫⁻ (a : α), f i a ∂μ) u
-- Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
/-- An indeterminate `i : σ` is weighted homogeneous of degree `w i`.  -/
MvPolynomial.isWeightedHomogeneous_X : ∀ (R : Type u_1) {M : Type u_2} [inst : CommSemiring R] {σ : Type u_3} [inst_1 : AddCommMonoid M] (w : σ → M) (i : σ),
  MvPolynomial.IsWeightedHomogeneous w (MvPolynomial.X i) (w i)
-- Mathlib.Combinatorics.SimpleGraph.Copy
SimpleGraph.killCopies.edgeSet.instFintype : {V : Type u_1} →
  {W : Type u_2} → {G : SimpleGraph V} → {H : SimpleGraph W} → [Fintype ↑G.edgeSet] → Fintype ↑(G.killCopies H).edgeSet
-- Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
CategoryTheory.ObjectProperty.strictColimitsOfShape_bot : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (J : Type u')
  [inst_1 : CategoryTheory.Category.{v', u'} J] [Nonempty J], ⊥.strictColimitsOfShape J = ⊥
-- Mathlib.GroupTheory.HNNExtension
HNNExtension.NormalWord.ReducedWord.prod.eq_1 : ∀ {G : Type u_1} [inst : Group G] {A B : Subgroup G} (φ : ↥A ≃* ↥B) (w : HNNExtension.NormalWord.ReducedWord G A B),
  HNNExtension.NormalWord.ReducedWord.prod φ w =
    HNNExtension.of w.head * (List.map (fun x => HNNExtension.t ^ ↑x.1 * HNNExtension.of x.2) w.toList).prod
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
MeasureTheory.FiniteMeasure.restrict_biUnion_finset : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] {ι : Type u_3} {μ : MeasureTheory.FiniteMeasure Ω} {T : Finset ι}
  {s : ι → Set Ω},
  (↑T).Pairwise (Function.onFun Disjoint s) →
    (∀ (i : ι), MeasurableSet (s i)) → μ.restrict (⋃ i ∈ T, s i) = ∑ i ∈ T, μ.restrict (s i)