mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Parser.Command
/-- In Lean, every concrete type other than the universes
and every type constructor other than dependent arrows
is an instance of a general family of type constructions known as inductive types.
It is remarkable that it is possible to construct a substantial edifice of mathematics
based on nothing more than the type universes, dependent arrow types, and inductive types;
everything else follows from those.
Intuitively, an inductive type is built up from a specified list of constructors.
For example, `List α` is the list of elements of type `α`, and is defined as follows:
```
inductive List (α : Type u) where
| nil
| cons (head : α) (tail : List α)
```
A list of elements of type `α` is either the empty list, `nil`,
or an element `head : α` followed by a list `tail : List α`.
See [Inductive types](https://lean-lang.org/theorem_proving_in_lean4/inductive_types.html)
for more information.
 -/
Lean.Parser.Command.inductive : Lean.Parser.Parser
-- Mathlib.Order.Filter.Ultrafilter.Defs
Ultrafilter.map_id : ∀ {α : Type u} (f : Ultrafilter α), Ultrafilter.map id f = f
-- Mathlib.Order.Lattice
/-- Transfer `Lattice` across an `Equiv`.  -/
Equiv.lattice : {α : Type u} → {β : Type v} → α ≃ β → [Lattice β] → Lattice α
-- Mathlib.Combinatorics.Matroid.Minor.Restrict
Matroid.isBasis_restrict_iff : ∀ {α : Type u_1} {M : Matroid α} {R I X : Set α},
  autoParam (R ⊆ M.E) Matroid.isBasis_restrict_iff._auto_1 → ((M.restrict R).IsBasis I X ↔ M.IsBasis I X ∧ X ⊆ R)
-- Mathlib.Topology.Homeomorph.Defs
Homeomorph.symm_comp_self : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (h : X ≃ₜ Y),
  ⇑h.symm ∘ ⇑h = id
-- Std.Data.HashMap.Raw
/-- Internal implementation detail of the hash map  -/
Std.HashMap.Raw.Equiv.inner : ∀ {α : Type u} {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β}, m₁.Equiv m₂ → m₁.inner.Equiv m₂.inner
-- Mathlib.Algebra.Group.Action.Prod
Prod.faithfulVAddLeft : ∀ {M : Type u_1} {α : Type u_5} {β : Type u_6} [inst : VAdd M α] [inst_1 : VAdd M β] [FaithfulVAdd M α] [Nonempty β],
  FaithfulVAdd M (α × β)
-- Mathlib.Order.Hom.WithTopBot
InfHom.withBot.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : SemilatticeInf α] [inst_1 : SemilatticeInf β] (f : InfHom α β),
  f.withBot = { toFun := WithBot.map ⇑f, map_inf' := ⋯ }
-- Mathlib.Algebra.Group.Action.Defs
IsCancelVAdd.right_cancel : ∀ {G : Type u_11} {P : Type u_12} [inst : VAdd G P] [IsCancelVAdd G P] (a b : G) (c : P), a +ᵥ c = b +ᵥ c → a = b
-- Mathlib.Data.Rat.Cast.Defs
/-- If monoid with zero homs `f` and `g` from `ℚ≥0` agree on the naturals then they are equal.  -/
MonoidWithZeroHomClass.ext_nnrat' : ∀ {F : Type u_1} {M₀ : Type u_5} [inst : MonoidWithZero M₀] [inst_1 : FunLike F ℚ≥0 M₀]
  [MonoidWithZeroHomClass F ℚ≥0 M₀] {f g : F}, (∀ (n : ℕ), f ↑n = g ↑n) → f = g
-- Mathlib.AlgebraicTopology.SimplicialSet.PiZero
SSet.π₀.lift_mk : ∀ {X : SSet} {T : Type u_1} (f : X.obj (Opposite.op { len := 0 }) → T)
  (hf : ∀ ⦃x₀ x₁ : X.obj (Opposite.op { len := 0 })⦄ (x : SSet.Edge x₀ x₁), f x₀ = f x₁)
  (x : X.obj (Opposite.op { len := 0 })), SSet.π₀.lift f hf (SSet.π₀.mk x) = f x
-- Mathlib.Analysis.Normed.Affine.Isometry
/-- An affine isometric equivalence between two normed vector spaces,
denoted `f : P ≃ᵃⁱ[𝕜] P₂`.  -/
«term_≃ᵃⁱ[_]_» : Lean.TrailingParserDescr
-- Init.Data.Vector.Lemmas
Vector.back?_eq_getElem? : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n}, xs.back? = xs[n - 1]?
-- Mathlib.Logic.Equiv.Multiset
encodeMultiset.eq_1 : ∀ {α : Type u_1} [inst : Encodable α] (s : Multiset α), encodeMultiset s = Encodable.encode (s.sort enle✝)
-- LeanSearchClient.LoogleSyntax
/-- Search [Loogle](https://loogle.lean-lang.org/json) from within Lean. This can be used as a command, term or tactic as in the following examples. In the case of a tactic, only valid tactics are displayed.


```lean
#loogle List ?a → ?a

example := #loogle List ?a → ?a

example : 3 ≤ 5 := by
  #loogle Nat.succ_le_succ
  sorry

```

## Loogle Usage

Loogle finds definitions and lemmas in various ways:

By constant:
🔍 Real.sin
finds all lemmas whose statement somehow mentions the sine function.

By lemma name substring:
🔍 \"differ\"
finds all lemmas that have \"differ\" somewhere in their lemma name.

By subexpression:
🔍 _ * (_ ^ _)
finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

The pattern can also be non-linear, as in
🔍 Real.sqrt ?a * Real.sqrt ?a

If the pattern has parameters, they are matched in any order. Both of these will find List.map:
🔍 (?a -> ?b) -> List ?a -> List ?b
🔍 List ?a -> (?a -> ?b) -> List ?b

By main conclusion:
🔍 |- tsum _ = _ * tsum _
finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
🔍 |- _ < _ → tsum _ < tsum _
will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, \"two\", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have \"two\" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

You can modify the Loogle server URL by setting the `LEANSEARCHCLIENT_LOOGLE_API_URL` environment variable.
 -/
LeanSearchClient.loogle_cmd : Lean.ParserDescr
-- Mathlib.Analysis.Calculus.FDeriv.Mul
Differentiable.inv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {R : Type u_5} [inst_3 : NormedDivisionRing R] [inst_4 : NormedAlgebra 𝕜 R] {h : E → R},
  Differentiable 𝕜 h → (∀ (x : E), h x ≠ 0) → Differentiable 𝕜 h⁻¹
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.instPartialOrder : {V : Type u} → PartialOrder (SimpleGraph V)
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toList_rco_add_add_eq_append : ∀ {m : ℤ} {n k : ℕ}, (m...m + ↑n + ↑k).toList = (m...m + ↑n).toList ++ ((m + ↑n)...m + ↑n + ↑k).toList
-- Mathlib.Data.Fintype.Order
/-- Constructs the `⊤` and `⊥` of a finite nonempty `Lattice`.  -/
Fintype.toBoundedOrder : (α : Type u_2) → [Fintype α] → [Nonempty α] → [inst : Lattice α] → BoundedOrder α
-- Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Real.self_sub_one_lt_mul_log : ∀ {x : ℝ}, 0 ≤ x → x ≠ 1 → x - 1 < x * Real.log x
-- Mathlib.RingTheory.Finiteness.FiniteTypeLocal
IsLocalization.finsetIntegerMultiple.congr_simp : ∀ {R : Type u_1} [inst : CommSemiring R] (M M_1 : Submonoid R) (e_M : M = M_1) {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [inst_3 : IsLocalization M S] [inst_4 : DecidableEq R] (s s_1 : Finset S),
  s = s_1 → IsLocalization.finsetIntegerMultiple M s = IsLocalization.finsetIntegerMultiple M_1 s_1
-- Mathlib.NumberTheory.Pell
/-- Every solution is, up to a sign, a power of a given fundamental solution.  -/
Pell.IsFundamental.eq_zpow_or_neg_zpow : ∀ {d : ℤ} {a₁ : Pell.Solution₁ d}, Pell.IsFundamental a₁ → ∀ (a : Pell.Solution₁ d), ∃ n, a = a₁ ^ n ∨ a = -a₁ ^ n
-- Mathlib.Analysis.Normed.Ring.Basic
/-- A non-unital subalgebra of a non-unital normed commutative ring is also a non-unital normed
commutative ring, with the restriction of the norm.  -/
NonUnitalSubalgebra.nonUnitalNormedCommRing : {𝕜 : Type u_5} →
  [inst : CommRing 𝕜] →
    {E : Type u_6} →
      [inst_1 : NonUnitalNormedCommRing E] →
        [inst_2 : Module 𝕜 E] → (s : NonUnitalSubalgebra 𝕜 E) → NonUnitalNormedCommRing ↥s
-- Mathlib.Algebra.GroupWithZero.Action.Defs
/-- Pullback a zero-preserving scalar multiplication along an injective zero-preserving map.
See note [reducible non-instances].  -/
Function.Injective.smulZeroClass : {M : Type u_1} →
  {A : Type u_7} →
    {B : Type u_9} →
      [inst : Zero A] →
        [inst_1 : SMulZeroClass M A] →
          [inst_2 : Zero B] →
            [inst_3 : SMul M B] →
              (f : ZeroHom B A) → Function.Injective ⇑f → (∀ (c : M) (x : B), f (c • x) = c • f x) → SMulZeroClass M B
-- Mathlib.Algebra.Module.Injective
Module.Baer.ExtensionOfMaxAdjoin.extendIdealTo_wd : ∀ {R : Type u} [inst : Ring R] {Q : Type v} [inst_1 : AddCommGroup Q] [inst_2 : Module R Q] {M : Type u_1}
  {N : Type u_2} [inst_3 : AddCommGroup M] [inst_4 : AddCommGroup N] [inst_5 : Module R M] [inst_6 : Module R N]
  (i : M →ₗ[R] N) (f : M →ₗ[R] Q) [inst_7 : Fact (Function.Injective ⇑i)] (h : Module.Baer R Q) {y : N} (r r' : R),
  r • y = r' • y →
    (Module.Baer.ExtensionOfMaxAdjoin.extendIdealTo i f h y) r =
      (Module.Baer.ExtensionOfMaxAdjoin.extendIdealTo i f h y) r'
-- Mathlib.CategoryTheory.Bicategory.InducedBicategory
CategoryTheory.Bicategory.InducedBicategory.bicategory_leftUnitor_hom_hom : ∀ {B : Type u_1} {C : Type u_2} [inst : CategoryTheory.Bicategory C] {F : B → C}
  {a b : CategoryTheory.Bicategory.InducedBicategory C F} (x : a ⟶ b),
  (CategoryTheory.Bicategory.leftUnitor x).hom.hom = (CategoryTheory.Bicategory.leftUnitor x.hom).hom
-- Mathlib.Topology.Order.OrderClosed
Icc_mem_nhdsLT : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [ClosedIicTopology α] {a b : α},
  a < b → Set.Icc a b ∈ nhdsWithin b (Set.Iio b)
-- Mathlib.Algebra.Group.Basic
mul_mul_inv_cancel'_right : ∀ {G : Type u_3} [inst : CommGroup G] (a b : G), a * (b * a⁻¹) = b
-- Init.Data.Int.Order
Int.toNat.eq_2 : ∀ (a : ℕ), (Int.negSucc a).toNat = 0
-- Mathlib.Analysis.Normed.Lp.lpSpace
lp.norm_le_of_forall_le : ∀ {α : Type u_3} {E : α → Type u_4} [inst : (i : α) → NormedAddCommGroup (E i)] {f : ↥(lp E ⊤)} {C : ℝ},
  0 ≤ C → (∀ (i : α), ‖↑f i‖ ≤ C) → ‖f‖ ≤ C
-- Mathlib.Order.UpperLower.CompleteLattice
LowerSet.carrier_eq_coe : ∀ {α : Type u_1} [inst : LE α] (s : LowerSet α), s.carrier = ↑s
-- Std.Time.Format.Modifier
Std.Time.Modifier.y.sizeOf_spec : ∀ (presentation : Std.Time.Year), sizeOf (Std.Time.Modifier.y presentation) = 1 + sizeOf presentation
-- Mathlib.GroupTheory.Focal
Subgroup.focalSubgroup_def : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G),
  H.focalSubgroup = Subgroup.closure {g | g ∈ H ∧ ∃ x ∈ H, ∃ u, g = ⁅x, u⁆}
-- Init.Data.String.Lemmas.Basic
String.pos!_eq_pos : ∀ {s : String} {p : String.Pos.Raw} (h : String.Pos.Raw.IsValid s p), s.pos! p = s.pos p h
-- Mathlib.Probability.Kernel.Representation
ProbabilityTheory.Kernel.exists_measurable_map_eq_unitInterval : ∀ {X : Type u_1} {Y : Type u_2} {mX : MeasurableSpace X} [Nonempty Y] {mY : MeasurableSpace Y} [StandardBorelSpace Y]
  (κ : ProbabilityTheory.Kernel X Y) [ProbabilityTheory.IsMarkovKernel κ],
  ∃ f, Measurable (Function.uncurry f) ∧ ∀ (a : X), MeasureTheory.Measure.map (f a) MeasureTheory.volume = κ a
-- Mathlib.Analysis.Normed.Lp.ProdLp
WithLp.prod_nnnorm_eq_of_L2 : ∀ {α : Type u_2} {β : Type u_3} [inst : SeminormedAddCommGroup α] [inst_1 : SeminormedAddCommGroup β]
  (x : WithLp 2 (α × β)), ‖x‖₊ = NNReal.sqrt (‖x.fst‖₊ ^ 2 + ‖x.snd‖₊ ^ 2)
-- Mathlib.Algebra.Ring.Parity
Even.trans_dvd : ∀ {α : Type u_2} [inst : Semiring α] {a b : α}, Even a → a ∣ b → Even b
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.toCycles_comp_homologyπ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasHomology],
  CategoryTheory.CategoryStruct.comp S.toCycles S.homologyπ = 0
-- Mathlib.Algebra.Order.Group.DenselyOrdered
le_iff_forall_lt_one_mul_le : ∀ {α : Type u_1} [inst : Group α] [inst_1 : LinearOrder α] [MulLeftMono α] [DenselyOrdered α] {a b : α},
  a ≤ b ↔ ∀ ε < 1, a * ε ≤ b
-- Mathlib.Tactic.Linter.TextBased
_private.Mathlib.Tactic.Linter.TextBased.0.Mathlib.Linter.TextBased.StyleError.semicolon.sizeOf_spec : sizeOf Mathlib.Linter.TextBased.StyleError.semicolon✝ = 1
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.getD_filterMap : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {γ : Type w} {m : Std.DHashMap α fun x => β}
  [inst : EquivBEq α] [inst_1 : LawfulHashable α] {f : α → β → Option γ} {k : α} {fallback : γ},
  Std.DHashMap.Const.getD (Std.DHashMap.filterMap f m) k fallback =
    ((Std.DHashMap.Const.get? m k).pbind fun x_2 h' => f (m.getKey k ⋯) x_2).getD fallback
-- Mathlib.Topology.Algebra.UniformConvergence
instDivUniformOnFun : {α : Type u_1} → {β : Type u_2} → {𝔖 : Set (Set α)} → [Div β] → Div (UniformOnFun α β 𝔖)
-- Mathlib.FieldTheory.SplittingField.IsSplittingField
Polynomial.IsSplittingField.finiteDimensional : ∀ {K : Type v} (L : Type w) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (f : Polynomial K)
  [Polynomial.IsSplittingField K L f], FiniteDimensional K L
-- Mathlib.Data.Sum.Order
OrderIso.sumAssoc_symm_apply_inl : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : LE α] [inst_1 : LE β] [inst_2 : LE γ] (a : α),
  (OrderIso.sumAssoc α β γ).symm (Sum.inl a) = Sum.inl (Sum.inl a)
-- Mathlib.AlgebraicTopology.ModelCategory.PathObject
HomotopicalAlgebra.PathObject.instNonempty : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C] {A : C},
  Nonempty (HomotopicalAlgebra.PathObject A)
-- Mathlib.Computability.Language
Symbol.terminal.inj : ∀ {T : Type u_4} {N : Type u_5} {t t_1 : T}, Symbol.terminal t = Symbol.terminal t_1 → t = t_1
-- Mathlib.Algebra.Homology.TotalComplex
HomologicalComplex₂.ιTotalOrZero_eq : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {I₁ : Type u_2}
  {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂)
  (c₁₂ : ComplexShape I₁₂) [inst_2 : TotalComplexShape c₁ c₂ c₁₂] [inst_3 : DecidableEq I₁₂] [inst_4 : K.HasTotal c₁₂]
  (i₁ : I₁) (i₂ : I₂) (i₁₂ : I₁₂) (h : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂),
  K.ιTotalOrZero c₁₂ i₁ i₂ i₁₂ = K.ιTotal c₁₂ i₁ i₂ i₁₂ h
-- Lean.Elab.MutualDef
/-- Push free variables in `s` to `toProcess` if they are not already there.  -/
_private.Lean.Elab.MutualDef.0.Lean.Elab.Term.MutualClosure.pushNewVars : Array Lean.FVarId → Lean.CollectFVars.State → Array Lean.FVarId
-- Mathlib.MeasureTheory.Function.UniformIntegrable
/-- A finite sequence of Lp functions is uniformly integrable in the probability sense.  -/
MeasureTheory.uniformIntegrable_finite : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup β] {p : ENNReal} {f : ι → α → β} [Finite ι],
  1 ≤ p → p ≠ ⊤ → (∀ (i : ι), MeasureTheory.MemLp (f i) p μ) → MeasureTheory.UniformIntegrable f p μ
-- Mathlib.Algebra.Group.Pointwise.Set.Finite
Set.Finite.mul : ∀ {α : Type u_2} [inst : Mul α] {s t : Set α}, s.Finite → t.Finite → (s * t).Finite
-- Mathlib.AlgebraicTopology.ModelCategory.Bifibrant
HomotopicalAlgebra.FibrantObject.weakEquivalence_homMk_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithFibrations C]
  [inst_2 : CategoryTheory.Limits.HasTerminal C] [inst_3 : HomotopicalAlgebra.CategoryWithWeakEquivalences C] {X Y : C}
  [inst_4 : HomotopicalAlgebra.IsFibrant X] [inst_5 : HomotopicalAlgebra.IsFibrant Y] (f : X ⟶ Y),
  HomotopicalAlgebra.WeakEquivalence (HomotopicalAlgebra.FibrantObject.homMk f) ↔ HomotopicalAlgebra.WeakEquivalence f
-- Mathlib.MeasureTheory.Group.Action
MeasureTheory.NullMeasurableSet.vadd : ∀ {G : Type u} {α : Type w} {m : MeasurableSpace α} [inst : AddGroup G] [inst_1 : AddAction G α]
  {μ : MeasureTheory.Measure α} [MeasureTheory.VAddInvariantMeasure G α μ] [MeasurableConstVAdd G α] {s : Set α},
  MeasureTheory.NullMeasurableSet s μ → ∀ (c : G), MeasureTheory.NullMeasurableSet (c +ᵥ s) μ
-- Mathlib.Control.LawfulFix
Pi.ωScottContinuous_uncurry : ∀ (α : Type u_1) (β : α → Type u_2) (γ : (a : α) → β a → Type u_3)
  [inst : (x : α) → (y : β x) → OmegaCompletePartialOrder (γ x y)],
  OmegaCompletePartialOrder.ωScottContinuous ⇑(Pi.monotoneUncurry α β γ)
-- Mathlib.CategoryTheory.Endofunctor.Algebra
CategoryTheory.Endofunctor.Coalgebra.functorOfNatTransComp_inv_app_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F₀ F₁ F₂ : CategoryTheory.Functor C C} (α : F₀ ⟶ F₁)
  (β : F₁ ⟶ F₂) (X : CategoryTheory.Endofunctor.Coalgebra F₀),
  ((CategoryTheory.Endofunctor.Coalgebra.functorOfNatTransComp α β).inv.app X).f = CategoryTheory.CategoryStruct.id X.V
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.val_inv_algHomUnitsEquiv_symm_apply : ∀ (R : Type u_1) (S : Type u_2) [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] (f : S ≃ₐ[R] S),
  ↑((AlgEquiv.algHomUnitsEquiv R S).symm f)⁻¹ = ↑f.symm
-- Init.Internal.Order.Basic
/-- A chain is a totally ordered set (representing a set as a predicate).

This is intended to be used in the construction of `partial_fixpoint`, and not meant to be used otherwise.
 -/
Lean.Order.chain : {α : Sort u} → [Lean.Order.PartialOrder α] → (α → Prop) → Prop
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Free
PresheafOfModules.freeObjDesc_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  {F : CategoryTheory.Functor Cᵒᵖ (Type u)} {G : PresheafOfModules R}
  (φ : F ⟶ G.presheaf.comp (CategoryTheory.forget Ab)) (X : Cᵒᵖ),
  (PresheafOfModules.freeObjDesc φ).app X = ModuleCat.freeDesc (φ.app X)
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.IsBoundedAtImInfty
EisensteinSeries.summable_norm_eisSummand : ∀ {k : ℤ}, 3 ≤ k → ∀ (z : UpperHalfPlane), Summable fun x => ‖EisensteinSeries.eisSummand k x z‖
-- Mathlib.Geometry.Manifold.Immersion
/-- If `f` is an immersion w.r.t. some complement `F`, it is an immersion.

Note that the proof contains a small formalisation-related subtlety: `F` can live in any universe,
while being an immersion requires the existence of a complement in the same universe as
the model normed space of `N`. This is solved by `smallComplement` and `smallEquiv`.
 -/
Manifold.IsImmersionOfComplement.isImmersion : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} {F : Type u_5}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup E'']
  [inst_4 : NormedSpace 𝕜 E''] [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace 𝕜 F] {H : Type u_7}
  [inst_7 : TopologicalSpace H] {G : Type u_9} [inst_8 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} [inst_9 : TopologicalSpace M] [inst_10 : ChartedSpace H M]
  {N : Type u_13} [inst_11 : TopologicalSpace N] [inst_12 : ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N},
  Manifold.IsImmersionOfComplement F I J n f → Manifold.IsImmersion I J n f
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
CategoryTheory.Limits.FormalCoproduct.inj_comp_cofanPtIsoSelf_hom_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Limits.FormalCoproduct C) (i : X.I)
  {Z : CategoryTheory.Limits.FormalCoproduct C} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.FormalCoproduct.cofan X.I X.toFun).inj i)
      (CategoryTheory.CategoryStruct.comp X.cofanPtIsoSelf.hom h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.FormalCoproduct.Hom.fromIncl i (CategoryTheory.CategoryStruct.id (X.obj i))) h
-- Mathlib.NumberTheory.Primorial
Nat.Prime.dvd_primorial : ∀ {p : ℕ}, Nat.Prime p → p ∣ primorial p
-- Aesop.Search.Expansion.Norm
_private.Aesop.Search.Expansion.Norm.0.Aesop.withNormTraceNode.fmt : Aesop.DisplayRuleName → Except Lean.Exception (Option Aesop.NormRuleResult) → Aesop.NormM Lean.MessageData
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.toCycles_comp_isoCycles₂_hom_apply : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) (x : (Fin 3 → G) →₀ ↑A),
  (CategoryTheory.ConcreteCategory.hom (groupHomology.isoCycles₂ A).hom)
      ((CategoryTheory.ConcreteCategory.hom (groupHomology.toCycles A 3 2)) x) =
    (groupHomology.shortComplexH2 A).moduleCatToCycles
      ((CategoryTheory.ConcreteCategory.hom (groupHomology.chainsIso₃ A).hom) x)
-- Mathlib.SetTheory.Ordinal.Topology
Ordinal.isOpen_singleton_iff : ∀ {a : Ordinal.{u}}, IsOpen {a} ↔ ¬Order.IsSuccLimit a
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.UInt
UInt32.reduceMul : Lean.Meta.Simp.DSimproc
-- Mathlib.Condensed.Light.Epi
LightCondMod.instPreservesEpimorphismsLightCondSetForget : ∀ (R : Type u) [inst : Ring R], (LightCondensed.forget R).PreservesEpimorphisms
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.X_add_C_ne_one : ∀ {R : Type u} [Nontrivial R] [inst : Semiring R] (r : R), Polynomial.X + Polynomial.C r ≠ 1
-- Mathlib.Analysis.SpecialFunctions.ExpDeriv
/-- `exp ∘ f` is analytic  -/
AnalyticOnNhd.rexp : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {s : Set E},
  AnalyticOnNhd ℝ f s → AnalyticOnNhd ℝ (fun z => Real.exp (f z)) s
-- Init.Data.Array.Range
Array.map_zipIdx : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {xs : Array α} {k : ℕ},
  Array.map (Prod.map f id) (xs.zipIdx k) = (Array.map f xs).zipIdx k
-- Mathlib.CategoryTheory.Limits.Preserves.Limits
CategoryTheory.preserves_lift_mapCone : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J]
  (F : CategoryTheory.Functor J C) [inst_3 : CategoryTheory.Limits.PreservesLimit F G]
  (c₁ c₂ : CategoryTheory.Limits.Cone F) (t : CategoryTheory.Limits.IsLimit c₁),
  (CategoryTheory.Limits.isLimitOfPreserves G t).lift (G.mapCone c₂) = G.map (t.lift c₂)
-- Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits
AlgebraicGeometry.PresheafedSpace.colimit_carrier : ∀ {J : Type u'} [inst : CategoryTheory.Category.{v', u'} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  [inst_2 : CategoryTheory.Limits.HasColimitsOfShape J TopCat]
  [inst_3 : ∀ (X : TopCat), CategoryTheory.Limits.HasLimitsOfShape Jᵒᵖ (TopCat.Presheaf C X)]
  (F : CategoryTheory.Functor J (AlgebraicGeometry.PresheafedSpace C)),
  ↑(AlgebraicGeometry.PresheafedSpace.colimit F) =
    CategoryTheory.Limits.colimit (F.comp (AlgebraicGeometry.PresheafedSpace.forget C))
-- Mathlib.MeasureTheory.Measure.Typeclasses.Probability
MeasureTheory.Measure.isProbabilityMeasure_map_iff : ∀ {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [inst : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {f : α → β},
  AEMeasurable f μ →
    (MeasureTheory.IsProbabilityMeasure (MeasureTheory.Measure.map f μ) ↔ MeasureTheory.IsProbabilityMeasure μ)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
CategoryTheory.Limits.instHasPullbackCompInv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z Z' : C} {f : X ⟶ Z} {g : Y ⟶ Z'} (i : Z ⟶ Z')
  [inst_1 : CategoryTheory.IsIso i] [CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp f i) g],
  CategoryTheory.Limits.HasPullback f (CategoryTheory.CategoryStruct.comp g (CategoryTheory.inv i))
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.map_id_equiv : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β),
  (↑(Std.DHashMap.Internal.Raw₀.map (fun x v => v) m)).Equiv ↑m
-- Mathlib.GroupTheory.Index
Subgroup.index_ne_zero_of_finite : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} [hH : Finite (G ⧸ H)], H.index ≠ 0
-- Mathlib.Analysis.Analytic.OfScalars
FormalMultilinearSeries.ofScalarsSum_eq_tsum : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Field 𝕜] [inst_1 : Ring E] [inst_2 : Algebra 𝕜 E] [inst_3 : TopologicalSpace E]
  [inst_4 : IsTopologicalRing E] (c : ℕ → 𝕜), FormalMultilinearSeries.ofScalarsSum c = fun x => ∑' (n : ℕ), c n • x ^ n
-- Mathlib.Lean.MessageData.ForExprs
Lean.MessageData.Exprs.mk : Lean.MessageData → Lean.MessageData.Exprs
-- Mathlib.Algebra.Polynomial.Bivariate
/-- The equiv between `R[X][Y]` and `R[X, Y]`.  -/
Polynomial.Bivariate.equivMvPolynomial : (R : Type u_1) → [inst : CommSemiring R] → Polynomial (Polynomial R) ≃ₐ[R] MvPolynomial (Fin 2) R