mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Sites.Precoverage
/-- A precoverage is stable under base change if pullbacks of covering presieves
are covering presieves.
Use `Precoverage.mem_coverings_of_isPullback` for less universe restrictions.
Note: This is stronger than the analogous requirement for a `Pretopology`, because
`IsPullback` does not imply equality with the (arbitrarily) chosen pullbacks in `C`.  -/
CategoryTheory.Precoverage.IsStableUnderBaseChange : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.Precoverage C → Prop
-- Batteries.Data.Fin.Coding
/-- Encode `PUnit` into `Fin 1`.  -/
Fin.encodePUnit : PUnit.{u_1} → Fin 1
-- Mathlib.Analysis.Convex.Function
/-- **Alias** of the reverse direction of `neg_strictConvexOn_iff`.

---

A function `-f` is strictly convex iff `f` is strictly concave.  -/
StrictConcaveOn.neg : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommGroup β] [inst_4 : PartialOrder β] [IsOrderedAddMonoid β] [inst_6 : SMul 𝕜 E] [inst_7 : Module 𝕜 β]
  {s : Set E} {f : E → β}, StrictConcaveOn 𝕜 s f → StrictConvexOn 𝕜 s (-f)
-- Mathlib.Tactic.TFAE
Mathlib.Tactic.TFAE.Parser.tfaeHaveIdLhs.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Batteries.Data.AssocList
/-- `O(1)`. Is the list empty?  -/
Batteries.AssocList.isEmpty : {α : Type u_1} → {β : Type u_2} → Batteries.AssocList α β → Bool
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
SimpleGraph.Walk.toSubgraph.eq_2 : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (v_3 : V) (h : G.Adj u v_3) (p : G.Walk v_3 v),
  (SimpleGraph.Walk.cons h p).toSubgraph = G.subgraphOfAdj h ⊔ p.toSubgraph
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.biproduct.map_epi : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {f g : J → C} [inst_2 : CategoryTheory.Limits.HasBiproduct f]
  [inst_3 : CategoryTheory.Limits.HasBiproduct g] (p : (j : J) → f j ⟶ g j) [∀ (j : J), CategoryTheory.Epi (p j)],
  CategoryTheory.Epi (CategoryTheory.Limits.biproduct.map p)
-- Plausible.Testable
Plausible.Testable.decGuardTestable : {p : Prop} →
  {var : String} →
    [Plausible.PrintableProp p] →
      [Decidable p] →
        {β : p → Prop} →
          [(h : p) → Plausible.Testable (β h)] → Plausible.Testable (Plausible.NamedBinder var (∀ (h : p), β h))
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.size_modify : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {f : β → β}, (t.modify k f).size = t.size
-- Mathlib.Analysis.Complex.Trigonometric
Complex.cos_sub_cos : ∀ (x y : ℂ), Complex.cos x - Complex.cos y = -2 * Complex.sin ((x + y) / 2) * Complex.sin ((x - y) / 2)
-- Mathlib.Algebra.Category.Grp.Biproducts
/-- We verify that the biproduct in `AddCommGrpCat` is isomorphic to
the Cartesian product of the underlying types:
 -/
AddCommGrpCat.biprodIsoProd : (G H : AddCommGrpCat) → G ⊞ H ≅ AddCommGrpCat.of (↑G × ↑H)
-- Mathlib.Combinatorics.Quiver.Path
Prefunctor.mapPath_cons : ∀ {V : Type u₁} [inst : Quiver V] {W : Type u₂} [inst_1 : Quiver W] (F : V ⥤q W) {a b c : V} (p : Quiver.Path a b)
  (e : b ⟶ c), F.mapPath (p.cons e) = (F.mapPath p).cons (F.map e)
-- Mathlib.SetTheory.Cardinal.Aleph
/-- The "pre-omega" function gives the initial ordinals listed by their ordinal index.
`preOmega n = n`, `preOmega ω = ω`, `preOmega (ω + 1) = ω₁`, etc.

For the more common omega function skipping over finite ordinals, see `Ordinal.omega`.  -/
Ordinal.preOmega : Ordinal.{u} ↪o Ordinal.{u}
-- Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
/-- A looser (but simpler than `card_edgeFinset_turanGraph`) bound on the number of edges in
`turanGraph n r`.  -/
SimpleGraph.mul_card_edgeFinset_turanGraph_le : ∀ {n r : ℕ}, 2 * r * (SimpleGraph.turanGraph n r).edgeFinset.card ≤ (r - 1) * n ^ 2
-- Qq.MatchImpl
Qq.Impl.PatVarDecl.mk.sizeOf_spec : ∀ (ty : Option Q(Lean.Expr)) (fvarId : Lean.FVarId) (userName : Lean.Name),
  sizeOf { ty := ty, fvarId := fvarId, userName := userName } = 1 + sizeOf ty + sizeOf fvarId + sizeOf userName
-- Mathlib.Dynamics.SymbolicDynamics.Basic
SymbolicDynamics.FullShift.cylinder.eq_1 : ∀ {A : Type u_1} {G : Type u_2} (U : Finset G) (x : G → A),
  SymbolicDynamics.FullShift.cylinder U x = {y | ∀ i ∈ U, y i = x i}
-- Mathlib.Combinatorics.Enumerative.DyckWord
DyckStep.U : DyckStep
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
/-- When a function has a limit at infinity `l`, and its derivative is nonnegative, then the
integral of the derivative on `(a, +∞)` is `l - g a` (and the derivative is integrable, see
`integrable_on_Ioi_deriv_of_nonneg'`). Version assuming differentiability on `[a, +∞)`.  -/
MeasureTheory.integral_Ioi_of_hasDerivAt_of_nonneg' : ∀ {g g' : ℝ → ℝ} {a l : ℝ},
  (∀ x ∈ Set.Ici a, HasDerivAt g (g' x) x) →
    (∀ x ∈ Set.Ioi a, 0 ≤ g' x) → Filter.Tendsto g Filter.atTop (nhds l) → ∫ (x : ℝ) in Set.Ioi a, g' x = l - g a
-- Mathlib.Algebra.Group.Subgroup.Map
AddSubgroup.map_bot : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] (f : G →+ N), AddSubgroup.map f ⊥ = ⊥
-- Init.Data.Option.Basic
Option.mapM_none : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Applicative m] (f : α → m β),
  Option.mapM f none = pure none
-- Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Finset.prod_apply_ite : ∀ {ι : Type u_1} {M : Type u_3} {γ : Type u_5} [inst : CommMonoid M] {s : Finset ι} {p : ι → Prop}
  [inst_1 : DecidablePred p] (f g : ι → γ) (h : γ → M),
  ∏ x ∈ s, h (if p x then f x else g x) = (∏ x ∈ s with p x, h (f x)) * ∏ x ∈ s with ¬p x, h (g x)
-- Mathlib.Order.Category.DistLat
/-- The equivalence between `DistLat` and itself induced by `OrderDual` both ways.  -/
DistLat.dualEquiv : DistLat ≌ DistLat
-- Mathlib.Data.Ordmap.Ordnode
Ordnode.toBinaryTree.eq_def : ∀ {α : Type u_1} (x : Ordnode α),
  x.toBinaryTree =
    match x with
    | Ordnode.nil => BinaryTree.nil
    | Ordnode.node size l x r => BinaryTree.node x l.toBinaryTree r.toBinaryTree
-- Mathlib.Algebra.Ring.Submonoid.Pointwise
AddSubmonoid.bot_mul : ∀ {R : Type u_2} [inst : NonUnitalNonAssocSemiring R] (S : AddSubmonoid R), ⊥ * S = ⊥
-- Init.Data.Int.DivMod.Lemmas
Int.ediv_nonneg_of_nonneg_of_nonneg : ∀ {x y : ℤ}, 0 ≤ x → 0 ≤ y → 0 ≤ x / y
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.image.isImage_lift : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y}
  [inst_1 : CategoryTheory.Limits.HasImage f] (F : CategoryTheory.Limits.MonoFactorisation f),
  (CategoryTheory.Limits.Image.isImage f).lift F = CategoryTheory.Limits.image.lift F
-- Init.Data.SInt.Lemmas
Int32.not_le : ∀ {n m : Int32}, ¬n ≤ m ↔ m < n
-- Mathlib.Analysis.Calculus.FDeriv.Affine
ContinuousAffineMap.hasFDerivWithinAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] (f : E →ᴬ[𝕜] F)
  {x : E} {s : Set E}, HasFDerivWithinAt (⇑f) f.contLinear s x
-- Mathlib.RingTheory.Smooth.NoetherianDescent
_private.Mathlib.RingTheory.Smooth.NoetherianDescent.0.Algebra.Smooth.DescentAux.mk.sizeOf_spec : ∀ {A : Type u} {B : Type u_2} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] [inst_3 : SizeOf A]
  [inst_4 : SizeOf B] (vars rels : Type) (P : Algebra.Presentation A B vars rels)
  (σ : B →ₐ[A] MvPolynomial vars A ⧸ P.ker ^ 2) (h : vars → MvPolynomial vars A)
  (p : rels → MvPolynomial rels (MvPolynomial vars A)) (hphom : ∀ (j : rels), (p j).IsHomogeneous 2)
  (hp : ∀ (j : rels), (MvPolynomial.eval P.relation) (p j) = (MvPolynomial.aeval h) (P.relation j))
  (q : vars → MvPolynomial rels P.Ring) (hqhom : ∀ (i : vars), (q i).IsHomogeneous 1)
  (hq : ∀ (i : vars), (MvPolynomial.eval P.relation) (q i) = h i - MvPolynomial.X i),
  sizeOf
      { vars := vars, rels := rels, P := P, σ := σ, h := h, p := p, hphom := hphom, hp := hp, q := q, hqhom := hqhom,
        hq := hq } =
    1 + sizeOf vars + sizeOf rels + sizeOf P + sizeOf σ
-- Mathlib.Analysis.InnerProductSpace.l2Space
/-- A mutually orthogonal family of subspaces of `E` induce a linear isometry from `lp 2` of the
subspaces into `E`.  -/
OrthogonalFamily.linearIsometry : {ι : Type u_1} →
  {𝕜 : Type u_2} →
    [inst : RCLike 𝕜] →
      {E : Type u_3} →
        [inst_1 : NormedAddCommGroup E] →
          [inst_2 : InnerProductSpace 𝕜 E] →
            {G : ι → Type u_4} →
              [inst_3 : (i : ι) → NormedAddCommGroup (G i)] →
                [inst_4 : (i : ι) → InnerProductSpace 𝕜 (G i)] →
                  [CompleteSpace E] → {V : (i : ι) → G i →ₗᵢ[𝕜] E} → OrthogonalFamily 𝕜 G V → ↥(lp G 2) →ₗᵢ[𝕜] E
-- Mathlib.Analysis.CStarAlgebra.Module.Synonym
/-- `WithCStarModule.equiv` as a continuous linear equivalence between `C⋆ᵐᵒᵈ E` and `E`.  -/
WithCStarModule.equivL : (R : Type u_1) →
  {A : Type u_3} →
    {E : Type u_4} →
      [inst : Semiring R] →
        [inst_1 : AddCommGroup E] → [inst_2 : UniformSpace E] → [inst_3 : Module R E] → WithCStarModule A E ≃L[R] E
-- Mathlib.Analysis.Real.Pi.Irrational
_private.Mathlib.Analysis.Real.Pi.Irrational.0.sinPoly.eq_2 : sinPoly✝ 1 = Polynomial.C 4
-- Mathlib.Analysis.Convex.Segment
Prod.openSegment_subset : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommMonoid F] [inst_4 : Module 𝕜 E] [inst_5 : Module 𝕜 F] (x y : E × F),
  openSegment 𝕜 x y ⊆ openSegment 𝕜 x.1 y.1 ×ˢ openSegment 𝕜 x.2 y.2
-- Mathlib.Topology.Order.OrderClosed
Pi.orderClosedTopology' : ∀ {α : Type u} {β : Type v} [inst : Preorder β] [inst_1 : TopologicalSpace β] [OrderClosedTopology β],
  OrderClosedTopology (α → β)
-- Init.Data.Int.Gcd
Int.gcd_gcd_self_right_right : ∀ (m n : ℤ), m.gcd ↑(n.gcd m) = n.gcd m
-- Mathlib.Combinatorics.SimpleGraph.DeleteEdges
SimpleGraph.DeleteFar.le_card_edgeFinset : ∀ {V : Type u_1} {G : SimpleGraph V} {𝕜 : Type u_2} [inst : Ring 𝕜] [inst_1 : PartialOrder 𝕜]
  [inst_2 : Fintype ↑G.edgeSet] {p : SimpleGraph V → Prop} {r : 𝕜}, G.DeleteFar p r → p ⊥ → r ≤ ↑G.edgeFinset.card
-- Lean.Meta.Tactic.Grind.EMatch
/-- When tracing is enabled track instances here. See comment at `InstanceMap`
 -/
Lean.Meta.Grind.EMatch.SearchState.instanceMap : Lean.Meta.Grind.EMatch.SearchState → Lean.Meta.Grind.EMatch.InstanceMap
-- Mathlib.GroupTheory.OrderOfElement
nsmulCoprime_apply : ∀ {n : ℕ} {G : Type u_6} [inst : AddGroup G] (h : (Nat.card G).Coprime n) (g : G), (nsmulCoprime h) g = n • g
-- Mathlib.RingTheory.Localization.NormTrace
/-- Let `S` be an extension of `R` and `Rₘ Sₘ` be localizations at `M` of `R S` respectively.
Then the norm of `a : Sₘ` over `Rₘ` is the norm of `a : S` over `R` if `S` is free as `R`-module.
 -/
Algebra.norm_localization : ∀ (R : Type u_1) {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {Rₘ : Type u_3}
  {Sₘ : Type u_4} [inst_3 : CommRing Rₘ] [inst_4 : Algebra R Rₘ] [inst_5 : CommRing Sₘ] [inst_6 : Algebra S Sₘ]
  (M : Submonoid R) [IsLocalization M Rₘ] [IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ] [inst_9 : Algebra Rₘ Sₘ]
  [inst_10 : Algebra R Sₘ] [IsScalarTower R Rₘ Sₘ] [IsScalarTower R S Sₘ] [Module.Free R S] [Module.Finite R S] (a : S),
  (Algebra.norm Rₘ) ((algebraMap S Sₘ) a) = (algebraMap R Rₘ) ((Algebra.norm R) a)
-- Mathlib.Algebra.Lie.Graded
DirectSum.decompose_bracket : ∀ {ι : Type u_1} {R : Type u_3} {L : Type u_4} [inst : DecidableEq ι] [inst_1 : AddCommMonoid ι] [inst_2 : CommRing R]
  [inst_3 : LieRing L] [inst_4 : LieAlgebra R L] (ℒ : ι → Submodule R L) [inst_5 : GradedLieAlgebra ℒ] (x y : L),
  (DirectSum.decompose ℒ) ⁅x, y⁆ = ⁅(DirectSum.decompose ℒ) x, (DirectSum.decompose ℒ) y⁆
-- Mathlib.RingTheory.Ideal.Basic
Ideal.span_range_pow_eq_top : ∀ {α : Type u_2} [inst : CommSemiring α] (s : Set α),
  Ideal.span s = ⊤ → ∀ (n : ↑s → ℕ), Ideal.span (Set.range fun x => ↑x ^ n x) = ⊤
-- Lean.Meta.Tactic.Grind.EMatchTheorem
/-- Given the type of a `match` congruence equation, annotate the discriminants using
the gadgets `Grind.genPattern` and `Grind.genHEqPattern`.
For example, consider the following `match` congruence theorem type
```
forall
  (motive : Option Nat → Sort u_1) (a✝ : Option Nat)
  (h_1 : a✝ = none → motive none)
  (h_2 : (val : Nat) → a✝ = some val → motive (some val))
  (val✝ : Nat)
  (heq_1 : a✝ = some val✝),
  g.match_1 motive a✝ h_1 h_2 ≍ h_2 val✝ heq_1
```
This function returns the type
```
forall
  (motive : Option Nat → Sort u_1) (a✝ : Option Nat)
  (h_1 : a✝ = none → motive none)
  (h_2 : (val : Nat) → a✝ = some val → motive (some val))
  (val✝ : Nat)
  (heq_1 : a✝ = some val✝),
  g.match_1 motive (Grind.genPattern (Option Nat) heq_1 a✝ (some val✝)) h_1 h_2
  ≍ h_2 val✝ heq_1
```
The gadget is used to infer a `generalize` pattern. The following term is used
during E-matching `g.match_1 motive (Grind.genPattern (Option Nat) heq_1 a✝ (some val✝)) h_1 h_2`
when matching `Grind.genPattern (Option Nat) heq_1 a✝ (some val✝)` the matcher uses
`(some val✝)` as the actual pattern, but also assigns `heq_1` `a✝` using the information stored
in the equivalence class.
 -/
_private.Lean.Meta.Tactic.Grind.EMatchTheorem.0.Lean.Meta.Grind.preprocessMatchCongrEqType : Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
IsAddLeftRegular.withBot : ∀ {α : Type u} [inst : Add α] {a : α}, IsAddLeftRegular a → IsAddLeftRegular ↑a
-- Mathlib.NumberTheory.Divisors
Nat.map_div_left_divisors : ∀ {n : ℕ}, Finset.map { toFun := fun d => (n / d, d), inj' := ⋯ } n.divisors = n.divisorsAntidiagonal
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.coboundaries₁.coe_mk : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A : Rep.{max u u_1, u, u} k G} (f : G → ↑A)
  (hf : f ∈ groupCohomology.coboundaries₁ A), ⇑⟨f, hf⟩ = f
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.MemLp.enorm_rpow_div : ∀ {α : Type u_1} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} {ε : Type u_6}
  [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε] {f : α → ε},
  MeasureTheory.MemLp f p μ → ∀ (q : ENNReal), MeasureTheory.MemLp (fun x => ‖f x‖ₑ ^ q.toReal) (p / q) μ
-- Batteries.Tactic.PrintPrefix
Batteries.Tactic.PrintPrefixConfig.mk.injEq : ∀
  (imported propositions propositionsOnly showTypes internals imported_1 propositions_1 propositionsOnly_1 showTypes_1
    internals_1 : Bool),
  ({ imported := imported, propositions := propositions, propositionsOnly := propositionsOnly, showTypes := showTypes,
        internals := internals } =
      { imported := imported_1, propositions := propositions_1, propositionsOnly := propositionsOnly_1,
        showTypes := showTypes_1, internals := internals_1 }) =
    (imported = imported_1 ∧
      propositions = propositions_1 ∧
        propositionsOnly = propositionsOnly_1 ∧ showTypes = showTypes_1 ∧ internals = internals_1)
-- Init.Data.Array.Attach
Array.attach_empty : ∀ {α : Type u_1}, #[].attach = #[]
-- Mathlib.Data.Finset.Fin
Finset.mem_attachFin : ∀ {n : ℕ} {s : Finset ℕ} (h : ∀ m ∈ s, m < n) {a : Fin n}, a ∈ s.attachFin h ↔ ↑a ∈ s
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
WeierstrassCurve.Projective.baseChange_neg : ∀ {R : Type r} {S : Type s} {A : Type u} {B : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing A]
  [inst_3 : CommRing B] {W' : WeierstrassCurve.Projective R} [inst_4 : Algebra R S] [inst_5 : Algebra R A]
  [inst_6 : Algebra S A] [IsScalarTower R S A] [inst_8 : Algebra R B] [inst_9 : Algebra S B] [IsScalarTower R S B]
  (f : A →ₐ[S] B) (P : Fin 3 → A), (W'.baseChange B).neg (⇑f ∘ P) = ⇑f ∘ (W'.baseChange A).neg P
-- Lean.MetavarContext
/-- Counter for setting the field `index` at `MetavarDecl`  -/
Lean.MetavarContext.mvarCounter : Lean.MetavarContext → ℕ
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
_private.Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers.0.CategoryTheory.Limits.parallelFamily.match_1.eq_1 : ∀ {J : Type u_1} (motive : (x y : CategoryTheory.Limits.WalkingParallelFamily J) → (x ⟶ y) → Sort u_2)
  (x : CategoryTheory.Limits.WalkingParallelFamily J)
  (h_1 :
    (x : CategoryTheory.Limits.WalkingParallelFamily J) →
      motive x x (CategoryTheory.Limits.WalkingParallelFamily.Hom.id x))
  (h_2 :
    (j : J) →
      motive CategoryTheory.Limits.WalkingParallelFamily.zero CategoryTheory.Limits.WalkingParallelFamily.one
        (CategoryTheory.Limits.WalkingParallelFamily.Hom.line j)),
  (match x, x, CategoryTheory.Limits.WalkingParallelFamily.Hom.id x with
    | x, .(x), CategoryTheory.Limits.WalkingParallelFamily.Hom.id .(x) => h_1 x
    | .(CategoryTheory.Limits.WalkingParallelFamily.zero), .(CategoryTheory.Limits.WalkingParallelFamily.one),
      CategoryTheory.Limits.WalkingParallelFamily.Hom.line j => h_2 j) =
    h_1 x
-- Mathlib.Algebra.Group.Hom.Instances
/-- `flip` arguments of `f : M →* N →* P`  -/
MonoidHom.flip : {M : Type uM} →
  {N : Type uN} →
    {P : Type uP} → {mM : MulOneClass M} → {mN : MulOneClass N} → {mP : CommMonoid P} → (M →* N →* P) → N →* M →* P
-- Mathlib.NumberTheory.EulerProduct.Basic
/-- The *Euler Product* for multiplicative (on coprime arguments) functions.

If `f : ℕ → R`, where `R` is a complete normed commutative ring, `f 0 = 0`, `f 1 = 1`, `f` is
multiplicative on coprime arguments, and `‖f ·‖` is summable, then
`∏' p : {p : ℕ | p.Prime}, ∑' e, f (p ^ e) = ∑' n, f n`.
This is a version using convergence of finite partial products.  -/
EulerProduct.eulerProduct : ∀ {R : Type u_1} [inst : NormedCommRing R] {f : ℕ → R} [CompleteSpace R],
  f 1 = 1 →
    (∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n) →
      (Summable fun x => ‖f x‖) →
        f 0 = 0 →
          Filter.Tendsto (fun n => ∏ p ∈ n.primesBelow, ∑' (e : ℕ), f (p ^ e)) Filter.atTop (nhds (∑' (n : ℕ), f n))
-- Mathlib.Topology.CWComplex.Abstract.Basic
/-- A CW-complex is a topological space such that `⊥_ _ ⟶ X` is a relative CW-complex.  -/
TopCat.CWComplex : TopCat → Type (u + 1)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKeyD_filterMap : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β}
  [inst_2 : LawfulBEq α] {f : (a : α) → β a → Option (γ a)} {k fallback : α} (h : m.WF),
  (Std.DHashMap.Raw.filterMap f m).getKeyD k fallback =
    ((m.getKey? k).pfilter fun x h' => (f x (m.get x ⋯)).isSome).getD fallback
-- Mathlib.Topology.Algebra.Polynomial
Polynomial.isProperMap_eval : ∀ {R : Type u_2} [inst : NormedRing R] [IsAbsoluteValue norm] [ProperSpace R] (p : Polynomial R),
  0 < p.degree → IsProperMap fun x => Polynomial.eval x p
-- Mathlib.CategoryTheory.Category.Pointed
Pointed.instInhabited : Inhabited Pointed
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : BEq α] [inst_2 : Std.LawfulBEqCmp cmp] {l : List (α × β)} {k : α}
  (contains_eq_false : (List.map Prod.fst l).contains k = false) {h' : k ∈ t.insertMany l},
  (t.insertMany l).getKey k h' = t.getKey k ⋯
-- Mathlib.Analysis.ODE.PicardLindelof
ODE.FunSpace.ext_iff : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {tmin tmax : ℝ} {t₀ : ↑(Set.Icc tmin tmax)} {x₀ : E} {r L : NNReal}
  {α β : ODE.FunSpace t₀ x₀ r L}, α = β ↔ ∀ (t : ↑(Set.Icc tmin tmax)), α.toFun t = β.toFun t
-- Mathlib.Data.Nat.Squarefree
Nat.coprime_of_squarefree_mul : ∀ {m n : ℕ}, Squarefree (m * n) → m.Coprime n
-- Mathlib.Control.Fix
Part.Fix.approx.eq_def : ∀ {α : Type u_1} {β : α → Type u_2} (f : ((a : α) → Part (β a)) → (a : α) → Part (β a)) (x : ℕ),
  Part.Fix.approx f x =
    match (motive := ℕ → (a : α) → Part (β a)) x with
    | 0 => ⊥
    | i.succ => f (Part.Fix.approx f i)
-- Aesop.Rule
Aesop.RegularRule.safe.inj : ∀ {r r_1 : Aesop.SafeRule}, Aesop.RegularRule.safe r = Aesop.RegularRule.safe r_1 → r = r_1
-- Aesop.Script.UScriptToSScript
Aesop.Script.UScript.toStepTree : Aesop.Script.UScript → Aesop.Script.StepTree
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.isEmpty_eq_false_iff_exists_contains_eq_true : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → (t.isEmpty = false ↔ ∃ a, Std.DTreeMap.Internal.Impl.contains a t = true)
-- Mathlib.Algebra.Group.ULift
ULift.div.eq_1 : ∀ {α : Type u} [inst : Div α], ULift.div = { div := fun f g => { down := f.down / g.down } }
-- Mathlib.Data.Real.ENatENNReal
/-- Coercion from `ℕ∞` to `ℝ≥0∞`.  -/
ENat.toENNReal : ℕ∞ → ENNReal
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.natDegree_eq_of_degree_eq_some : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} {n : ℕ}, p.degree = ↑n → p.natDegree = n
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.mk_iUnion_eq_sum_mk_lift : ∀ {α : Type u} {ι : Type v} {f : ι → Set α},
  Pairwise (Function.onFun Disjoint f) →
    Cardinal.lift.{v, u} (Cardinal.mk ↑(⋃ i, f i)) = Cardinal.sum fun i => Cardinal.mk ↑(f i)
-- Mathlib.Algebra.Order.ToIntervalMod
QuotientAddGroup.instBtwQuotientAddSubgroupZmultiples : {α : Type u_1} →
  [inst : AddCommGroup α] →
    [inst_1 : LinearOrder α] →
      [IsOrderedAddMonoid α] →
        [hα : Archimedean α] → {p : α} → [hp' : Fact (0 < p)] → Btw (α ⧸ AddSubgroup.zmultiples p)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.mem_iff_contains : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} {k : α}, k ∈ t ↔ t.contains k = true
-- Mathlib.Data.Finmap
Multiset.keys_zero : ∀ {α : Type u} {β : α → Type v}, Multiset.keys 0 = 0
-- Mathlib.Analysis.Complex.UpperHalfPlane.Basic
/-- Real part  -/
UpperHalfPlane.re : UpperHalfPlane → ℝ
-- Mathlib.Algebra.Category.ModuleCat.ProjectiveDimension
/-- **Alias** of `ModuleCat.hasProjectiveDimensionLE_of_semiLinearEquiv`. -/
CategoryTheory.hasProjectiveDimensionLE_of_semiLinearEquiv : ∀ {R : Type u} [inst : Ring R] [Small.{v, u} R] {R' : Type u'} [inst_2 : Ring R'] [Small.{v', u'} R'] (e : R ≃+* R')
  {M : ModuleCat R} {N : ModuleCat R'} (e' : ↑M ≃ₛₗ[↑e] ↑N) (n : ℕ) [CategoryTheory.HasProjectiveDimensionLE M n],
  CategoryTheory.HasProjectiveDimensionLE N n
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.Poly.toExpr : Nat.Internal.Linear.Poly → Nat.Internal.Linear.Expr
-- Mathlib.Topology.MetricSpace.BundledFun
/-- Strong triangle inequality of an ultrametric.  -/
PseudoMetric.IsUltra.le_sup' : ∀ {X : Type u_1} {R : Type u_2} {inst : Zero R} {inst_1 : Add R} {inst_2 : LE R} {inst_3 : Max R} {d : PseudoMetric X R}
  [self : d.IsUltra] (x y z : X), d x z ≤ d x y ⊔ d y z
-- Mathlib.Logic.Function.Basic
Pi.map_id' : ∀ {ι : Type u_3} {α : ι → Type u_4}, (Pi.map fun i a => a) = fun x => x
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.insertManyIfNewUnit_list_eq_empty_iff : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α Unit cmp} [inst : Std.TransCmp cmp] {l : List α},
  t.insertManyIfNewUnit l = ∅ ↔ t = ∅ ∧ l = []
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.BinaryBicones.functoriality.congr_simp : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {D : Type uD} [inst_2 : CategoryTheory.Category.{uD', uD} D] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  (P Q : C) (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms],
  CategoryTheory.Limits.BinaryBicones.functoriality P Q F = CategoryTheory.Limits.BinaryBicones.functoriality P Q F
-- Mathlib.Analysis.Real.Pi.Irrational
_private.Mathlib.Analysis.Real.Pi.Irrational.0.I.eq_1 : ∀ (n : ℕ) (θ : ℝ), I✝ n θ = ∫ (x : ℝ) in -1..1, (1 - x ^ 2) ^ n * Real.cos (x * θ)
-- Mathlib.Algebra.Group.Indicator
Set.indicator_sub' : ∀ {α : Type u_1} {G : Type u_6} [inst : AddGroup G] (s : Set α) (f g : α → G),
  s.indicator (f - g) = s.indicator f - s.indicator g
-- Mathlib.Topology.NhdsWithin
nhdsSetWithin.eq_1 : ∀ {X : Type u_1} [inst : TopologicalSpace X] (s t : Set X), nhdsSetWithin s t = nhdsSet s ⊓ Filter.principal t
-- Init.Data.Order.MinMaxOn
left_le_apply_maxOn : ∀ {β : Type u_1} {α : Sort u_2} [le : LE β] [inst : DecidableLE β] [Std.IsLinearPreorder β] {f : α → β} {x y : α},
  f x ≤ f (maxOn f x y)