mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.CWComplex.Classical.Finite
Topology.CWComplex.mkFinite_map : ∀ {X : Type u} [inst : TopologicalSpace X] (C : Set X) (cell : ℕ → Type u)
  (map : (n : ℕ) → cell n → PartialEquiv (Fin n → ℝ) X)
  (eventually_isEmpty_cell : ∀ᶠ (n : ℕ) in Filter.atTop, IsEmpty (cell n)) (finite_cell : ∀ (n : ℕ), Finite (cell n))
  (source_eq : ∀ (n : ℕ) (i : cell n), (map n i).source = Metric.ball 0 1)
  (continuousOn : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i)) (Metric.closedBall 0 1))
  (continuousOn_symm : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i).symm) (map n i).target)
  (pairwiseDisjoint' : Set.univ.PairwiseDisjoint fun ni => ↑(map ni.fst ni.snd) '' Metric.ball 0 1)
  (mapsTo_iff_image_subset :
    ∀ (n : ℕ) (i : cell n),
      Set.MapsTo (↑(map n i)) (Metric.sphere 0 1) (⋃ m, ⋃ (_ : m < n), ⋃ j, ↑(map m j) '' Metric.closedBall 0 1))
  (union' : ⋃ n, ⋃ j, ↑(map n j) '' Metric.closedBall 0 1 = C) (n : ℕ) (i : Topology.RelCWComplex.cell C n),
  Topology.CWComplex.map n i = Topology.RelCWComplex.map n i
-- Mathlib.CategoryTheory.Shift.SingleFunctors
/-- the isomorphism `functor a' ⋙ shiftFunctor D n ≅ functor a` when `n + a = a'`  -/
CategoryTheory.SingleFunctors.shiftIso : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        {A : Type u_5} →
          [inst_2 : AddMonoid A] →
            [inst_3 : CategoryTheory.HasShift D A] →
              (self : CategoryTheory.SingleFunctors C D A) →
                (n a a' : A) → n + a = a' → ((self.functor a').comp (CategoryTheory.shiftFunctor D n) ≅ self.functor a)
-- Mathlib.Computability.TuringMachine.ToPartrec
_private.Mathlib.Computability.TuringMachine.ToPartrec.0.Turing.PartrecToTM2.trList.match_1.eq_1 : ∀ (motive : List ℕ → Sort u_1) (h_1 : Unit → motive []) (h_2 : (n : ℕ) → (ns : List ℕ) → motive (n :: ns)),
  (match [] with
    | [] => h_1 ()
    | n :: ns => h_2 n ns) =
    h_1 ()
-- Mathlib.RepresentationTheory.Homological.TateCohomology.Basic
/-- The shortcut path of taking Tate cohomology which aligns with
`groupCohomology` and `groupHomology`.  -/
tateCohomology : {R G : Type u} → [inst : CommRing R] → [inst_1 : Group G] → [Fintype G] → Rep.{u, u, u} R G → ℤ → ModuleCat R
-- Init.Data.SInt.Bitwise
ISize.toInt32_or : ∀ (a b : ISize), (a ||| b).toInt32 = a.toInt32 ||| b.toInt32
-- Lean.Parser.Term
/-- `letRecDecl` matches the body of a let-rec declaration: a doc comment, attributes, and then
a let declaration without the `let` keyword, such as `/-- foo -/ @[simp] bar := 1`.  -/
Lean.Parser.Term.letRecDecl : Lean.Parser.Parser
-- Std.Http.Protocol.H1.Error
/-- Malformed start line (request-line or status-line).
 -/
Std.Http.Protocol.H1.Error.invalidStatusLine : Std.Http.Protocol.H1.Error
-- Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
ModularForm.toCuspForm.congr_simp : ∀ {k : ℤ} (f f_1 : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k) (e_f : f = f_1)
  (h : (PowerSeries.coeff 0) (UpperHalfPlane.qExpansion 1 ⇑f) = 0), f.toCuspForm h = f_1.toCuspForm ⋯
-- Mathlib.Algebra.Order.Kleene
one_le_kstar : ∀ {α : Type u_1} [inst : KleeneAlgebra α] {a : α}, 1 ≤ KStar.kstar a
-- Mathlib.LinearAlgebra.Quotient.Basic
Submodule.mapQ_apply : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (p : Submodule R M)
  {R₂ : Type u_3} {M₂ : Type u_4} [inst_3 : Ring R₂] [inst_4 : AddCommGroup M₂] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  (q : Submodule R₂ M₂) (f : M →ₛₗ[τ₁₂] M₂) {h : p ≤ Submodule.comap f q} (x : M),
  (p.mapQ q f h) (Submodule.Quotient.mk x) = Submodule.Quotient.mk (f x)
-- Lean.Meta.Tactic.Grind.EMatchTheorem
/-- `outParam` arguments are uniquely determined by type class resolution and should not
be part of the e-matching pattern. Including them is redundant (the instance, which is
already wildcarded, determines the `outParam` value) and harmful when the normalizer
changes their syntactic form.

**Motivation.** Consider the `ToInt` class used by the `grind` linear arithmetic module:
```
class ToInt (α : Type) (range : outParam IntInterval) where ...
instance : ToInt (Fin n) (.co 0 n) where ...
@[grind =] theorem toInt_fin (x : Fin n) : ToInt.toInt x = x.val
```
The elaborated pattern for `toInt_fin` is:
```
@ToInt.toInt (Fin #1) (IntInterval.co 0 (NatCast.natCast #1)) _ #0
```
The `range` argument `IntInterval.co 0 (NatCast.natCast #1)` is included in the pattern
because the pattern generator treats it as relevant. However, the `grind` normalizer pushes
`NatCast.natCast` inside arithmetic operations, rewriting `↑(n + 1)` to `↑n + 1`. So when
`grind` processes `Fin (n + 1)`, the e-graph contains:
```
@ToInt.toInt (Fin (n + 1)) (IntInterval.co 0 (↑n + 1)) inst x
```
The pattern expects `NatCast.natCast #1` at the second position of `IntInterval.co`, but
the e-graph has `HAdd.hAdd (NatCast.natCast n) 1` — a different head symbol. The pattern
cannot match, and `toInt_fin` never fires.

Since `outParam` arguments are determined by type class resolution (just like instance
arguments, which are already wildcarded), they can be safely ignored in patterns. This is
justified by the same reasoning: after e-matching finds candidate substitutions, the
instantiation step checks all arguments via `isDefEq`, preserving soundness.
 -/
Lean.Meta.Grind.NormalizePattern.PatternArgKind.outParam : Lean.Meta.Grind.NormalizePattern.PatternArgKind
-- Mathlib.Order.Interval.Set.Basic
Set.Ici_False : Set.Ici False = Set.univ
-- Mathlib.AlgebraicTopology.SimplicialSet.PushoutProduct
SSet.Subcomplex.unionProd.pushoutObjObj_inr : ∀ {X Y : SSet} (S : X.Subcomplex) (T : Y.Subcomplex),
  (SSet.Subcomplex.unionProd.pushoutObjObj S T).inr = SSet.Subcomplex.unionProd.ι₂ S T
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.card_le_card_sub_self : ∀ {α : Type u_2} [inst : AddGroup α] [inst_1 : DecidableEq α] {s : Finset α}, s.card ≤ (s - s).card
-- Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv
/-- `convs'` returns the same value for a gcf and the corresponding squashed gcf at the
squashed position.  -/
GenContFract.succ_nth_conv'_eq_squashGCF_nth_conv' : ∀ {K : Type u_1} {n : ℕ} {g : GenContFract K} [inst : DivisionRing K], g.convs' (n + 1) = (g.squashGCF n).convs' n
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.preimage_const_mul_Ioc : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α] (a b c : α),
  (fun x => a * x) ⁻¹' Set.Ioc b c = Set.Ioc (b / a) (c / a)
-- Mathlib.LinearAlgebra.BilinearMap
/-- Composing a linear map `Q → N` and a bilinear map `M → N → P` to
form a bilinear map `M → Q → P`.  -/
LinearMap.compl₂ : {R : Type u_14} →
  {R₂ : Type u_15} →
    {R₃ : Type u_16} →
      {R₄ : Type u_17} →
        {R₅ : Type u_18} →
          {M : Type u_19} →
            {N : Type u_20} →
              {P : Type u_21} →
                {Q : Type u_22} →
                  [inst : Semiring R] →
                    [inst_1 : Semiring R₂] →
                      [inst_2 : Semiring R₃] →
                        [inst_3 : Semiring R₄] →
                          [inst_4 : Semiring R₅] →
                            {σ₂₃ : R₂ →+* R₃} →
                              {σ₄₂ : R₄ →+* R₂} →
                                {σ₄₃ : R₄ →+* R₃} →
                                  [inst_5 : AddCommMonoid M] →
                                    [inst_6 : AddCommMonoid N] →
                                      [inst_7 : AddCommMonoid P] →
                                        [inst_8 : AddCommMonoid Q] →
                                          [inst_9 : Module R M] →
                                            [inst_10 : Module R₂ N] →
                                              [inst_11 : Module R₃ P] →
                                                [inst_12 : Module R₄ Q] →
                                                  [inst_13 : Module R₅ P] →
                                                    [RingHomCompTriple σ₄₂ σ₂₃ σ₄₃] →
                                                      [inst_15 : SMulCommClass R₃ R₅ P] →
                                                        {σ₁₅ : R →+* R₅} →
                                                          (M →ₛₗ[σ₁₅] N →ₛₗ[σ₂₃] P) →
                                                            (Q →ₛₗ[σ₄₂] N) → M →ₛₗ[σ₁₅] Q →ₛₗ[σ₄₃] P
-- Mathlib.Algebra.Category.Grp.Limits
CommGrpCat.forget_preservesLimits : CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget CommGrpCat)
-- Mathlib.Order.KrullDimension
Order.krullDim_WithTop : ∀ {α : Type u_1} [inst : Preorder α] [Nonempty α], Order.krullDim (WithTop α) = Order.krullDim α + 1
-- Mathlib.Computability.TuringMachine.Computable
Turing.FinTM2.decidableEqK : (tm : Turing.FinTM2) → DecidableEq tm.K
-- Mathlib.Order.Category.FinBddDistLat
_private.Mathlib.Order.Category.FinBddDistLat.0.FinBddDistLat.Hom.mk.injEq : ∀ {X Y : FinBddDistLat} (hom' hom'_1 : BoundedLatticeHom ↑X.toDistLat ↑Y.toDistLat),
  ({ hom' := hom' } = { hom' := hom'_1 }) = (hom' = hom'_1)
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.IrreducibleCloseds.map.congr_simp : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f f_1 : β → α)
  (e_f : f = f_1) (hf : Continuous f) (c c_1 : TopologicalSpace.IrreducibleCloseds β),
  c = c_1 → TopologicalSpace.IrreducibleCloseds.map f hf c = TopologicalSpace.IrreducibleCloseds.map f_1 ⋯ c_1
-- Lean.Parser.Basic
Lean.Parser.OrElseOnAntiquotBehavior : Type
-- Mathlib.Algebra.Algebra.Basic
NeZero.of_faithfulSMul : ∀ (R : Type u_1) (A : Type u_2) [inst : Semiring R] [inst_1 : Semiring A] [inst_2 : Module R A] [IsScalarTower R A A]
  [FaithfulSMul R A] (n : ℕ) [NeZero ↑n], NeZero ↑n
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.ofHom_apply : ∀ {k : Type u} {G : Type v} [inst : Semiring k] [inst_1 : Monoid G] {X Y : Type w} [inst_2 : AddCommGroup X]
  [inst_3 : AddCommGroup Y] [inst_4 : Module k X] [inst_5 : Module k Y] {ρ : Representation k G X}
  {σ : Representation k G Y} (f : ρ.IntertwiningMap σ) (x : X),
  (CategoryTheory.ConcreteCategory.hom (Rep.ofHom f)) x = f x
-- Mathlib.RingTheory.QuasiFinite.Basic
Algebra.QuasiFinite.discreteTopology_primeSpectrum : ∀ (R : Type u_1) (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [DiscreteTopology (PrimeSpectrum R)] [Algebra.QuasiFinite R S], DiscreteTopology (PrimeSpectrum S)
-- Mathlib.CategoryTheory.Enriched.Basic
CategoryTheory.e_id_comp_assoc : ∀ (V : Type v) [inst : CategoryTheory.Category.{w, v} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u₁}
  [inst_2 : CategoryTheory.EnrichedCategory V C] (X Y : C) {Z : V} (h : (X ⟶[V] Y) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (X ⟶[V] Y)).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.eId V X) (X ⟶[V] Y))
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.eComp V X X Y) h)) =
    h
-- Mathlib.GroupTheory.Perm.Support
Equiv.Perm.support_extend_domain : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {β : Type u_2} [inst_2 : DecidableEq β]
  [inst_3 : Fintype β] {p : β → Prop} [inst_4 : DecidablePred p] (f : α ≃ Subtype p) {g : Equiv.Perm α},
  (g.extendDomain f).support = Finset.map f.asEmbedding g.support
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
/-- In a space with second countable topology, measurable implies strongly measurable.  -/
AEMeasurable.aestronglyMeasurable : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {f : α → β} [inst_1 : MeasurableSpace β] [TopologicalSpace.PseudoMetrizableSpace β] [OpensMeasurableSpace β]
  [SecondCountableTopology β], AEMeasurable f μ → MeasureTheory.AEStronglyMeasurable f μ
-- Std.Data.DHashMap.Internal.Model
Std.DHashMap.Internal.Raw₀.Const.modify_eq_alter : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  (m : Std.DHashMap.Internal.Raw₀ α fun x => β) (a : α) (f : β → β),
  Std.DHashMap.Internal.Raw₀.Const.modify m a f = Std.DHashMap.Internal.Raw₀.Const.alter m a fun x => Option.map f x
-- Init.Data.UInt.Bitwise
UInt32.neg_one_or : ∀ {a : UInt32}, -1 ||| a = -1
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.map_add : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} [inst : MeasurableSpace β] {M : Type u_3}
  [inst_1 : AddCommMonoid M] [inst_2 : TopologicalSpace M] [inst_3 : ContinuousAdd M]
  (v w : MeasureTheory.VectorMeasure α M) (f : α → β), (v + w).map f = v.map f + w.map f
-- Lean.Meta.Match.MatcherInfo
Lean.Meta.Match.instInhabitedDiscrInfo : Inhabited Lean.Meta.Match.DiscrInfo
-- Mathlib.Combinatorics.Additive.DoublingConst
/-- If `A` has small difference, then it has small doubling, with the constant squared.

This is a consequence of the Ruzsa triangle inequality.  -/
Finset.addConst_le_subConst_sq : ∀ {G : Type u_1} [inst : AddCommGroup G] [inst_1 : DecidableEq G] {A : Finset G}, A.addConst A ≤ A.subConst A ^ 2
-- Mathlib.Data.Matrix.Composition
Matrix.isUnit_comp_symm_iff : ∀ (I : Type u_1) (J : Type u_2) (R : Type u_5) [inst : Semiring R] [inst_1 : Fintype I] [inst_2 : Fintype J]
  [inst_3 : DecidableEq I] [inst_4 : DecidableEq J] {M : Matrix (I × J) (I × J) R},
  IsUnit ((Matrix.comp I I J J R).symm M) ↔ IsUnit M
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.core.injEq : ∀ (e e_1 : Lean.Expr),
  (Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.core e = Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.core e_1) = (e = e_1)
-- Mathlib.Order.BooleanAlgebra.Set
Set.compl_ne_univ : ∀ {α : Type u_1} {s : Set α}, sᶜ ≠ Set.univ ↔ s.Nonempty
-- Batteries.Data.BinomialHeap.Basic
/-- An empty forest, which has depth `0`.  -/
Batteries.BinomialHeap.Imp.HeapNode.nil : {α : Type u} → Batteries.BinomialHeap.Imp.HeapNode α
-- Mathlib.Algebra.Ring.Parity
Nat.mod_two_add_add_odd_mod_two : ∀ (m : ℕ) {n : ℕ}, Odd n → m % 2 + (m + n) % 2 = 1
-- Mathlib.GroupTheory.Index
Subgroup.relIndex_iInf_ne_zero : ∀ {G : Type u_1} [inst : Group G] {L : Subgroup G} {ι : Type u_3} [_hι : Finite ι] {f : ι → Subgroup G},
  (∀ (i : ι), (f i).relIndex L ≠ 0) → (⨅ i, f i).relIndex L ≠ 0
-- Init.Notation
/-- `structInstFieldDecl` is the syntax category for value declarations for fields in structure instance notation.
For example, the `:= 1` and `| 0 => 0 | n + 1 => n` in `{ x := 1, f | 0 => 0 | n + 1 => n }` are in the `structInstFieldDecl` class.  -/
Lean.Parser.Category.structInstFieldDecl : Lean.Parser.Category
-- Mathlib.Computability.EpsilonNFA
/-- An `εNFA` is a set of states (`σ`), a transition function from state to state labelled by the
alphabet (`step`), a starting state (`start`) and a set of acceptance states (`accept`).
Note the transition function sends a state to a `Set` of states and can make ε-transitions by
inputting `none`.
Since this definition allows for Automata with infinite states, a `Fintype` instance must be
supplied for true `εNFA`'s.  -/
εNFA : Type u → Type v → Type (max u v)
-- Mathlib.Algebra.Star.CHSH
CHSH_id : ∀ {R : Type u} [inst : CommRing R] {A₀ A₁ B₀ B₁ : R},
  A₀ ^ 2 = 1 →
    A₁ ^ 2 = 1 →
      B₀ ^ 2 = 1 →
        B₁ ^ 2 = 1 →
          (2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁) * (2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁) =
            4 * (2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁)
-- Mathlib.Tactic.CategoryTheory.Coherence
Mathlib.Tactic.Coherence.insert_id_lhs : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : C} (f g : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.id Y) = g → f = g
-- Mathlib.Geometry.Manifold.Diffeomorph
/-- Apply a continuous linear equivalence to the model vector space.  -/
ModelWithCorners.transContinuousLinearEquiv : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {E' : Type u_3} →
            [inst_3 : NormedAddCommGroup E'] →
              [inst_4 : NormedSpace 𝕜 E'] →
                {H : Type u_5} →
                  [inst_5 : TopologicalSpace H] → ModelWithCorners 𝕜 E H → (E ≃L[𝕜] E') → ModelWithCorners 𝕜 E' H
-- Mathlib.Topology.MetricSpace.Snowflaking
Metric.Snowflaking.image_toSnowflaking_eq_preimage : ∀ {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} (s : Set X),
  ⇑Metric.Snowflaking.toSnowflaking '' s = ⇑Metric.Snowflaking.ofSnowflaking ⁻¹' s
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKeyD_eq_of_equiv : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β)
  [EquivBEq α] [LawfulHashable α],
  (↑m₁).WF → (↑m₂).WF → (↑m₁).Equiv ↑m₂ → ∀ {k fallback : α}, m₁.getKeyD k fallback = m₂.getKeyD k fallback
-- Mathlib.NumberTheory.Padics.Complex
/-- We define `𝓞_ℂ_[p]` as the subring of elements of `ℂ_[p]` with valuation `≤ 1`.  -/
«term𝓞_ℂ_[_]» : Lean.ParserDescr
-- Mathlib.Algebra.Order.GroupWithZero.Basic
one_le_inv₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] {a : G₀},
  0 < a → (1 ≤ a⁻¹ ↔ a ≤ 1)
-- Mathlib.Topology.MetricSpace.IsometricSMul
Metric.preimage_smul_eball : ∀ {G : Type v} {X : Type w} [inst : PseudoEMetricSpace X] [inst_1 : Group G] [inst_2 : MulAction G X]
  [IsIsometricSMul G X] (c : G) (x : X) (r : ENNReal), (fun x => c • x) ⁻¹' Metric.eball x r = Metric.eball (c⁻¹ • x) r
-- Mathlib.Topology.Algebra.Field
/-- The map `fun x => a * x + b`, as a homeomorphism from `𝕜` (a topological field) to itself,
when `a ≠ 0`.
 -/
affineHomeomorph : {𝕜 : Type u_2} → [inst : Field 𝕜] → [inst_1 : TopologicalSpace 𝕜] → [IsTopologicalRing 𝕜] → (a : 𝕜) → 𝕜 → a ≠ 0 → 𝕜 ≃ₜ 𝕜
-- Mathlib.Algebra.BigOperators.Expect
Finset.expect_eq_sum_div_card : ∀ {ι : Type u_1} {K : Type u_3} [inst : Semifield K] [inst_1 : CharZero K] (s : Finset ι) (f : ι → K),
  (s.expect fun i => f i) = (∑ i ∈ s, f i) / ↑s.card
-- Mathlib.Analysis.Distribution.TemperateGrowth
MeasureTheory.Measure.integrablePower.eq_1 : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : MeasurableSpace E] (μ : MeasureTheory.Measure E),
  μ.integrablePower = if h : μ.HasTemperateGrowth then ⋯.choose else 0
-- Mathlib.Topology.UniformSpace.UniformConvergence
/-- A sequence of functions `Fₙ` converges uniformly on a set `s` to a limiting function `f` w.r.t.
filter `p` iff the function `(n, x) ↦ (f x, Fₙ x)` converges along `p ×ˢ 𝓟 s` to the uniformity.
In other words: one knows nothing about the behavior of `x` in this limit besides it being in `s`.
 -/
tendstoUniformlyOn_iff_tendsto : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α}
  {p : Filter ι},
  TendstoUniformlyOn F f p s ↔ Filter.Tendsto (fun q => (f q.2, F q.1 q.2)) (p ×ˢ Filter.principal s) (uniformity β)
-- Mathlib.Combinatorics.Additive.CovBySMul
CovByVAdd.mono : ∀ {M : Type u_1} {X : Type u_3} [inst : AddMonoid M] [inst_1 : AddAction M X] {K L : ℝ} {A B : Set X},
  K ≤ L → CovByVAdd M K A B → CovByVAdd M L A B
-- Mathlib.Algebra.Polynomial.Expand
Polynomial.expand_X : ∀ {R : Type u} [inst : CommSemiring R] (p : ℕ), (Polynomial.expand R p) Polynomial.X = Polynomial.X ^ p
-- Mathlib.Combinatorics.SimpleGraph.Finite
SimpleGraph.degree_pos_iff_nonempty : ∀ {V : Type u_1} {G : SimpleGraph V} {v : V} [inst : Fintype ↑(G.neighborSet v)],
  0 < G.degree v ↔ (G.neighborSet v).Nonempty
-- Mathlib.Data.Setoid.Partition
/-- The equivalence between the quotient by an equivalence relation and its
type of equivalence classes.  -/
Setoid.quotientEquivClasses : {α : Type u_1} → (r : Setoid α) → Quotient r ≃ ↑r.classes
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.principalUnitGroup_le_principalUnitGroup : ∀ {K : Type u} [inst : Field K] {A B : ValuationSubring K}, B.principalUnitGroup ≤ A.principalUnitGroup ↔ A ≤ B
-- Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
MeasureTheory.instSFiniteSumOfCountable : ∀ {α : Type u_1} {ι : Type u_3} {m0 : MeasurableSpace α} [Countable ι] (m : ι → MeasureTheory.Measure α)
  [∀ (n : ι), MeasureTheory.SFinite (m n)], MeasureTheory.SFinite (MeasureTheory.Measure.sum m)
-- Mathlib.Algebra.Homology.HomotopyFiber
/-- The first projection `K.pathObject ⟶ K`.  -/
HomologicalComplex.pathObject.π₀ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {α : Type u_2} →
        {c : ComplexShape α} →
          (K : HomologicalComplex C c) →
            [inst_2 : DecidableRel c.Rel] →
              [inst_3 : ∀ (i : α), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] →
                [inst_4 : K.HasPathObject] → K.pathObject ⟶ K
-- Mathlib.Algebra.Order.AddGroupWithTop
add_le_add_iff_right_of_ne_top : ∀ {α : Type u_2} [inst : LinearOrderedAddCommMonoidWithTop α] {a b c : α}, a ≠ ⊤ → (a + b ≤ a + c ↔ b ≤ c)
-- Lean.Meta.Tactic.Grind.EMatchTheorem
Lean.Meta.Grind.NormalizePattern.PatternArgKind.proof.sizeOf_spec : sizeOf Lean.Meta.Grind.NormalizePattern.PatternArgKind.proof = 1
-- Mathlib.Data.Num.Basic
/-- The predecessor of a `Num` as a `Num`, where `pred 0 = 0`.  -/
Num.pred : Num → Num
-- Mathlib.Data.Int.NatAbs
Int.natAbsHom_apply : ∀ (m : ℤ), Int.natAbsHom m = m.natAbs
-- Std.Tactic.BVDecide.LRAT.Internal.Assignment
Std.Tactic.BVDecide.LRAT.Internal.Assignment.removePosAssignment.eq_4 : Std.Tactic.BVDecide.LRAT.Internal.Assignment.unassigned.removePosAssignment =
  Std.Tactic.BVDecide.LRAT.Internal.Assignment.unassigned
-- Mathlib.Order.Hom.Lattice
SupHom.sup_apply : ∀ {α : Type u_2} {β : Type u_3} [inst : Max α] [inst_1 : SemilatticeSup β] (f g : SupHom α β) (a : α),
  (f ⊔ g) a = f a ⊔ g a
-- Mathlib.LinearAlgebra.Contraction
/-- If the identity linear map lies in the range of the canonical map `M* ⊗[R] M → Hom_R(M, M)`,
then `M` is a finite projective `R`-module (finite part).  -/
Module.Finite.of_one_mem_range_dualTensorHom : ∀ {R : Type u_2} {M : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  1 ∈ (dualTensorHom R M M).range → Module.Finite R M
-- Mathlib.Geometry.Manifold.Submersion
Manifold.IsSubmersionAt.mem_codChart_source : ∀ {𝕜 : Type u_1} {E'' : Type u_3} {H : Type u_7} {G : Type u_9} {E : Type u} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup E'']
  [inst_4 : NormedSpace 𝕜 E''] [inst_5 : TopologicalSpace H] [inst_6 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} {N : Type u_13} [inst_7 : TopologicalSpace M]
  [inst_8 : ChartedSpace H M] [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N}
  {x : M} (h : Manifold.IsSubmersionAt I J n f x), f x ∈ h.codChart.source
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.mkAppStx : Lean.Ident → Lean.TSyntaxArray `doc_arg → Lean.Doc.DocM Lean.Term
-- Lean.Expr
Lean.Expr.updateMData! : Lean.Expr → Lean.Expr → Lean.Expr
-- Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice
csSup_mul : ∀ {M : Type u_1} [inst : ConditionallyCompleteLattice M] [inst_1 : Group M] [MulLeftMono M] [MulRightMono M]
  {s t : Set M}, s.Nonempty → BddAbove s → t.Nonempty → BddAbove t → sSup (s * t) = sSup s * sSup t
-- Mathlib.Data.Matrix.Mul
Matrix.map_mul : ∀ {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} {β : Type w} [inst : NonUnitalNonAssocSemiring α]
  [inst_1 : Fintype n] {L : Matrix m n α} {M : Matrix n o α} [inst_2 : NonUnitalNonAssocSemiring β] {F : Type u_10}
  [inst_3 : FunLike F α β] [NonUnitalRingHomClass F α β] {f : F}, (L * M).map ⇑f = L.map ⇑f * M.map ⇑f
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
two_nsmul_sup_eq_add_add_abs_sub : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : AddCommGroup α] [AddLeftMono α] (a b : α), 2 • (a ⊔ b) = a + b + |b - a|
-- Mathlib.NumberTheory.Height.NumberField
/-- The logarithmic height of a positive natural number `n` cast to `ℚ` equals `log n`.  -/
Rat.logHeight₁_natCast : ∀ (n : ℕ) [NeZero n], Height.logHeight₁ ↑n = Real.log ↑n
-- Mathlib.Analysis.Normed.Group.Basic
/-- **Alias** of `NormedGroup.nhds_one_basis_norm_lt`. -/
NormedCommGroup.nhds_one_basis_norm_lt : ∀ {E : Type u_5} [inst : SeminormedGroup E], (nhds 1).HasBasis (fun ε => 0 < ε) fun ε => {y | ‖y‖ < ε}