mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Internal.Do.Order.Basic
/-- The top element of the `Prop` lattice is `True`. Not a global `@[simp]` lemma: collapsing the
lattice `⊤`/`⊥`/`⌜·⌝` to `True`/`False`/`p` would change how `mvcgen` discharge lattice
goals. Tagged `@[grind =]` for use under `grind`.  -/
Lean.Order.top_prop_eq : Lean.Order.top = True
-- Mathlib.CategoryTheory.Triangulated.Functor
CategoryTheory.Functor.mapTriangleInvRotateIso_hom_app_hom₃ : ∀ {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] [inst_2 : CategoryTheory.HasShift C ℤ]
  [inst_3 : CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [inst_4 : F.CommShift ℤ]
  [inst_5 : CategoryTheory.Preadditive C] [inst_6 : CategoryTheory.Preadditive D] [inst_7 : F.Additive]
  (X : CategoryTheory.Pretriangulated.Triangle C),
  (F.mapTriangleInvRotateIso.hom.app X).hom₃ = CategoryTheory.CategoryStruct.id (F.obj X.obj₂)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getElem?_ofList_of_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp] {l : List (α × β)} {k k' : α},
  cmp k k' = Ordering.eq →
    ∀ {v : β},
      List.Pairwise (fun a b => ¬cmp a.1 b.1 = Ordering.eq) l → (k, v) ∈ l → (Std.TreeMap.ofList l cmp)[k']? = some v
-- Init.Grind.Interactive
/-- Shows asserted facts.  -/
Lean.Parser.Tactic.Grind.showAsserted : Lean.ParserDescr
-- Mathlib.CategoryTheory.EquivalenceRelation
/-- `B` is the "quotient" of the relation  -/
CategoryTheory.EffectiveEquivalenceRelation.B : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {R A : C} → {p₁ p₂ : R ⟶ A} → CategoryTheory.EffectiveEquivalenceRelation p₁ p₂ → C
-- Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting
CategoryTheory.HasLiftingProperty.transfiniteComposition.SqStruct.mk.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : LinearOrder J] [inst_2 : OrderBot J]
  {F : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.Cocone F} {X Y : C} {p : X ⟶ Y} {f : F.obj ⊥ ⟶ X}
  {g : c.pt ⟶ Y} {j : J} (f' f'_1 : F.obj j ⟶ X) (e_f' : f' = f'_1)
  (w₁ : CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.homOfLE ⋯)) f' = f)
  (w₂ : CategoryTheory.CategoryStruct.comp f' p = CategoryTheory.CategoryStruct.comp (c.ι.app j) g),
  { f' := f', w₁ := w₁, w₂ := w₂ } = { f' := f'_1, w₁ := ⋯, w₂ := ⋯ }
-- Mathlib.RingTheory.DiscreteValuationRing.TFAE
/-- The following are equivalent for a
Noetherian local domain that is not a field `(R, m, k)`:
0. `R` is a discrete valuation ring
1. `R` is a valuation ring
2. `R` is a Dedekind domain
3. `R` is integrally closed with a unique non-zero prime ideal
4. `m` is principal
5. `dimₖ m/m² = 1`
6. Every nonzero ideal is a power of `m`.

Also see `tfae_of_isNoetherianRing_of_isLocalRing_of_isDomain` for a version without `¬ IsField R`.
 -/
IsDiscreteValuationRing.TFAE : ∀ (R : Type u_1) [inst : CommRing R] [IsNoetherianRing R] [inst_2 : IsLocalRing R] [inst_3 : IsDomain R],
  ¬IsField R →
    [IsDiscreteValuationRing R, ValuationRing R, IsDedekindDomain R, IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ P.IsPrime,
        Submodule.IsPrincipal (IsLocalRing.maximalIdeal R),
        Module.finrank (IsLocalRing.ResidueField R) (IsLocalRing.CotangentSpace R) = 1,
        ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = IsLocalRing.maximalIdeal R ^ n].TFAE
-- Lean.Parser.Term
Lean.Parser.Term.ident.formatter : Lean.PrettyPrinter.Formatter
-- Std.Data.String.ToInt
Int.repr_inj : ∀ {a b : ℤ}, a.repr = b.repr ↔ a = b
-- Mathlib.Algebra.DirectSum.Module
DirectSum.component.lof_self : ∀ (R : Type u) [inst : Semiring R] {ι : Type v} {M : ι → Type w} [inst_1 : (i : ι) → AddCommMonoid (M i)]
  [inst_2 : (i : ι) → Module R (M i)] [inst_3 : DecidableEq ι] (i : ι) (b : M i),
  (DirectSum.component R ι M i) ((DirectSum.lof R ι M i) b) = b
-- Mathlib.Order.Heyting.Regular
Heyting.Regular.coe_inf : ∀ {α : Type u_1} [inst : HeytingAlgebra α] (a b : Heyting.Regular α), ↑(a ⊓ b) = ↑a ⊓ ↑b
-- Mathlib.Tactic.Peel
/-- Peels matching quantifiers off of a given term and the goal and introduces the relevant variables.

- `peel e` peels all quantifiers (at reducible transparency),
  using `this` for the name of the peeled hypothesis.
- `peel e with h` is `peel e` but names the peeled hypothesis `h`.
  If `h` is `_` then uses `this` for the name of the peeled hypothesis.
- `peel n e` peels `n` quantifiers (at default transparency).
- `peel n e with x y z ... h` peels `n` quantifiers, names the peeled hypothesis `h`,
  and uses `x`, `y`, `z`, and so on to name the introduced variables; these names may be `_`.
  If `h` is `_` then uses `this` for the name of the peeled hypothesis.
  The length of the list of variables does not need to equal `n`.
- `peel e with x₁ ... xₙ h` is `peel n e with x₁ ... xₙ h`.

There are also variants that apply to an iff in the goal:
- `peel n` peels `n` quantifiers in an iff.
- `peel with x₁ ... xₙ` peels `n` quantifiers in an iff and names them.

Given `p q : ℕ → Prop`, `h : ∀ x, p x`, and a goal `⊢ : ∀ x, q x`, the tactic `peel h with x h'`
will introduce `x : ℕ`, `h' : p x` into the context and the new goal will be `⊢ q x`. This works
with `∃`, as well as `∀ᶠ` and `∃ᶠ`, and it can even be applied to a sequence of quantifiers. Note
that this is a logically weaker setup, so using this tactic is not always feasible.

For a more complex example, given a hypothesis and a goal:
```
h : ∀ ε > (0 : ℝ), ∃ N : ℕ, ∀ n ≥ N, 1 / (n + 1 : ℝ) < ε
⊢ ∀ ε > (0 : ℝ), ∃ N : ℕ, ∀ n ≥ N, 1 / (n + 1 : ℝ) ≤ ε
```
(which differ only in `<`/`≤`), applying `peel h with ε hε N n hn h_peel` will yield a tactic state:
```
h : ∀ ε > (0 : ℝ), ∃ N : ℕ, ∀ n ≥ N, 1 / (n + 1 : ℝ) < ε
ε : ℝ
hε : 0 < ε
N n : ℕ
hn : N ≤ n
h_peel : 1 / (n + 1 : ℝ) < ε
⊢ 1 / (n + 1 : ℝ) ≤ ε
```
and the goal can be closed with `exact h_peel.le`.
Note that in this example, `h` and the goal are logically equivalent statements, but `peel`
*cannot* be immediately applied to show that the goal implies `h`.

In addition, `peel` supports goals of the form `(∀ x, p x) ↔ ∀ x, q x`, or likewise for any
other quantifier. In this case, there is no hypothesis or term to supply, but otherwise the syntax
is the same. So for such goals, the syntax is `peel 1` or `peel with x`, and after which the
resulting goal is `p x ↔ q x`. The `congr!` tactic can also be applied to goals of this form using
`congr! 1 with x`. While `congr!` applies congruence lemmas in general, `peel` can be relied upon
to only apply to outermost quantifiers.

Finally, the user may supply a term `e` via `... using e` in order to close the goal
immediately. In particular, `peel h using e` is equivalent to `peel h; exact e`. The `using` syntax
may be paired with any of the other features of `peel`.

This tactic works by repeatedly applying lemmas such as `forall_imp`, `Exists.imp`,
`Filter.Eventually.mp`, `Filter.Frequently.mp`, and `Filter.Eventually.of_forall`.
 -/
Mathlib.Tactic.Peel.peel : Lean.ParserDescr
-- Mathlib.AlgebraicTopology.CechNerve
CategoryTheory.CosimplicialObject.equivalenceRightToLeft_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 :
    ∀ (n : ℕ) (f : CategoryTheory.Arrow C),
      CategoryTheory.Limits.HasWidePushout f.left (fun x => f.right) fun x => f.hom]
  (F : CategoryTheory.Arrow C) (X : CategoryTheory.CosimplicialObject.Augmented C)
  (G : F ⟶ CategoryTheory.CosimplicialObject.Augmented.toArrow.obj X),
  (CategoryTheory.CosimplicialObject.equivalenceRightToLeft F X G).left = CategoryTheory.Arrow.Hom.left G
-- Mathlib.Tactic.CategoryTheory.ToApp
/-- Given a term of type `∀ ..., η = θ`, where `η θ : f ⟶ g` are 2-morphisms in some bicategory
`B`, which is bound by the `∀` binder, get the corresponding equation in the bicategory `Cat`.

It is important here that the levels in the term are level metavariables, as otherwise these will
not be reassignable to the corresponding levels of `Cat`.  -/
Mathlib.Tactic.CategoryTheory.ToApp.toCatExpr : Lean.Expr → Lean.MetaM Lean.Expr
-- Lean.Elab.MutualDef
_private.Lean.Elab.MutualDef.0.Lean.Elab.Term.withHeaderSecVars.getFVars : Lean.Expr → Lean.MetaM (Array Lean.FVarId)
-- Mathlib.Probability.Kernel.Defs
ProbabilityTheory.Kernel.sum_fintype : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [inst : Fintype ι]
  (κ : ι → ProbabilityTheory.Kernel α β), ProbabilityTheory.Kernel.sum κ = ∑ i, κ i
-- Lean.Parser.Term
Lean.Parser.Term.letI.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
/-- `toCompletion` as a uniform-space isomorphism onto the underlying completion.  -/
IsDedekindDomain.HeightOneSpectrum.adicCompletion.uniformEquiv : {R : Type u_1} →
  [inst : CommRing R] →
    [inst_1 : IsDedekindDomain R] →
      (K : Type u_2) →
        [inst_2 : Field K] →
          [inst_3 : Algebra R K] →
            [inst_4 : IsFractionRing R K] →
              (v : IsDedekindDomain.HeightOneSpectrum R) →
                IsDedekindDomain.HeightOneSpectrum.adicCompletion K v ≃ᵤ
                  (IsDedekindDomain.HeightOneSpectrum.valuation K v).Completion
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
ProjectiveSpectrum.coe_vanishingIdeal : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubmonoidClass σ A] {𝒜 : ℕ → σ}
  [inst_3 : GradedRing 𝒜] (t : Set (ProjectiveSpectrum 𝒜)),
  ↑(ProjectiveSpectrum.vanishingIdeal t) = {f | ∀ x ∈ t, f ∈ x.asHomogeneousIdeal}
-- Mathlib.RingTheory.IsAdjoinRoot
IsAdjoinRoot.lift_map : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] {f : Polynomial R} [inst_2 : Algebra R S]
  (h : IsAdjoinRoot S f) {T : Type u_1} [inst_3 : CommRing T] {i : R →+* T} {x : T} (hx : Polynomial.eval₂ i x f = 0)
  (z : Polynomial R), (h.lift i x hx) (h.map z) = Polynomial.eval₂ i x z
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.universally.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C) (X Y : C) (f : X ⟶ Y),
  P.universally f =
    ∀ ⦃X' Y' : C⦄ (i₁ : X' ⟶ X) (i₂ : Y' ⟶ Y) (f' : X' ⟶ Y'), CategoryTheory.IsPullback f' i₁ i₂ f → P f'
-- Mathlib.Order.Category.DistLat
/-- Construct a bundled `DistLat` from the underlying type and typeclass.  -/
DistLat.of : (X : Type u_1) → [DistribLattice X] → DistLat
-- Mathlib.Data.Rat.Floor
Rat.ceil_cast : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [inst_3 : FloorRing α] (x : ℚ),
  ⌈↑x⌉ = ⌈x⌉
-- Mathlib.Data.Finset.Card
Finset.eq_iff_card_ge_of_superset : ∀ {α : Type u_1} {s t : Finset α}, s ⊆ t → (t.card ≤ s.card ↔ t = s)
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.instZeroValueGroupWithZero : {R : Type u_1} → [inst : Semiring R] → [inst_1 : ValuativeRel R] → Zero (ValuativeRel.ValueGroupWithZero R)
-- Batteries.Data.PairingHeap
Batteries.PairingHeapImp.Heap.size_tail? : ∀ {α : Type u_1} {le : α → α → Bool} {s' s : Batteries.PairingHeapImp.Heap α},
  s.NoSibling → Batteries.PairingHeapImp.Heap.tail? le s = some s' → s.size = s'.size + 1
-- Mathlib.GroupTheory.Coxeter.Inversion
CoxeterSystem.IsReflection.length_mul_right_ne : ∀ {B : Type u_1} {W : Type u_2} [inst : Group W] {M : CoxeterMatrix B} {cs : CoxeterSystem M W} {t : W},
  cs.IsReflection t → ∀ (w : W), cs.length (t * w) ≠ cs.length w
-- Mathlib.FieldTheory.Minpoly.ConjRootClass
ConjRootClass.minpoly_injective : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L],
  Function.Injective ConjRootClass.minpoly
-- Mathlib.Algebra.Lie.Weights.Basic
/-- If `M` is a representation of a nilpotent Lie algebra `L`, and `x : L`, then
`posFittingCompOf R M x` is the infimum of the decreasing system
`range φₓ ⊇ range φₓ² ⊇ range φₓ³ ⊇ ⋯` where `φₓ : End R M := toEnd R L M x`. We call this
the "positive Fitting component" because with appropriate assumptions (e.g., `R` is a field and
`M` is finite-dimensional) `φₓ` induces the so-called Fitting decomposition: `M = M₀ ⊕ M₁` where
`M₀ = genWeightSpaceOf M 0 x` and `M₁ = posFittingCompOf R M x`.

It is a Lie submodule because `L` is nilpotent.  -/
LieModule.posFittingCompOf : (R : Type u_2) →
  {L : Type u_3} →
    (M : Type u_4) →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [inst_2 : LieAlgebra R L] →
            [inst_3 : AddCommGroup M] →
              [inst_4 : Module R M] →
                [inst_5 : LieRingModule L M] → [LieModule R L M] → [LieRing.IsNilpotent L] → L → LieSubmodule R L M
-- Mathlib.CategoryTheory.EqToHom
CategoryTheory.eqToIso.hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (p : X = Y),
  (CategoryTheory.eqToIso p).hom = CategoryTheory.eqToHom p
-- Init.Data.List.Nat.InsertIdx
List.getElem?_insertIdx_of_gt : ∀ {α : Type u} {l : List α} {x : α} {i j : ℕ}, i < j → (l.insertIdx i x)[j]? = l[j - 1]?
-- Mathlib.Probability.Kernel.Disintegration.CondCDF
ProbabilityTheory.condCDF_ae_eq : ∀ {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) [MeasureTheory.IsFiniteMeasure ρ] (r : ℚ),
  (fun a => ↑(ProbabilityTheory.condCDF ρ a) ↑r) =ᵐ[ρ.fst] fun a => (ProbabilityTheory.preCDF ρ r a).toReal
-- Mathlib.Analysis.Calculus.BumpFunction.Convolution
/-- If a function `g` is locally integrable, then the convolution `φ i * g` converges almost
everywhere to `g` if `φ i` is a sequence of bump functions with support tending to `0`, provided
that the ratio between the inner and outer radii of `φ i` remains bounded.  -/
ContDiffBump.ae_convolution_tendsto_right_of_locallyIntegrable : ∀ {G : Type uG} {E' : Type uE'} [inst : NormedAddCommGroup E'] {g : G → E'} [inst_1 : MeasurableSpace G]
  {μ : MeasureTheory.Measure G} [inst_2 : NormedSpace ℝ E'] [inst_3 : NormedAddCommGroup G] [inst_4 : NormedSpace ℝ G]
  [CompleteSpace E'] [BorelSpace G] [inst_7 : FiniteDimensional ℝ G] [μ.IsAddHaarMeasure] {ι : Type u_1}
  {φ : ι → ContDiffBump 0} {l : Filter ι} {K : ℝ},
  Filter.Tendsto (fun i => (φ i).rOut) l (nhds 0) →
    (∀ᶠ (i : ι) in l, (φ i).rOut ≤ K * (φ i).rIn) →
      MeasureTheory.LocallyIntegrable g μ →
        ∀ᵐ (x₀ : G) ∂μ,
          Filter.Tendsto (fun i => MeasureTheory.convolution ((φ i).normed μ) g (ContinuousLinearMap.lsmul ℝ ℝ) μ x₀) l
            (nhds (g x₀))
-- Mathlib.Lean.Json
Lean.instToJsonPUnit_mathlib : Lean.ToJson PUnit.{u_1 + 1}
-- Mathlib.Algebra.GCDMonoid.Multiset
Multiset.lcm_ne_zero_iff : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] [Nontrivial α] (s : Multiset α),
  s.lcm ≠ 0 ↔ 0 ∉ s
-- Mathlib.Algebra.Ring.Basic
Subsingleton.to_noZeroDivisors : ∀ (α : Type u_3) [inst : Mul α] [inst_1 : Zero α] [Subsingleton α], NoZeroDivisors α
-- Mathlib.AlgebraicTopology.EilenbergSteenrod
/-- `homₚ` needs to be compatible with the boundary maps.  -/
TopPair.HomologyPretheory.Hom.w_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} {HP HP' : TopPair.HomologyPretheory C c} (self : HP.Hom HP') (i j : ι)
  {Z : CategoryTheory.Functor TopPair C} (h : TopPair.proj₂.comp (HP'.H j) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (HP.δ i j)
      (CategoryTheory.CategoryStruct.comp (TopPair.proj₂.whiskerLeft (self.hom j)) h) =
    CategoryTheory.CategoryStruct.comp (self.homₚ i) (CategoryTheory.CategoryStruct.comp (HP'.δ i j) h)
-- Lean.DocString.Parser
/-- Return some inline text up to the next inline opener or the end of
the line, whichever is first. Always consumes at least one
logical character on success, taking escaping into account.  -/
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.inlineText : Lean.Parser.ParserFn
-- Mathlib.Analysis.Asymptotics.ExpGrowth
ExpGrowth.expGrowthSup_of_eventually_ge : ∀ {u v : ℕ → ENNReal} {b : ENNReal},
  b ≠ 0 → (∀ᶠ (n : ℕ) in Filter.atTop, b * u n ≤ v n) → ExpGrowth.expGrowthSup u ≤ ExpGrowth.expGrowthSup v
-- Mathlib.Data.ZMod.IntUnitsPower
toMul_uzpow : ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : Module R (Additive ℤˣ)] (u : Additive ℤˣ) (r : R),
  Additive.toMul (r • u) = Additive.toMul u ^ r
-- Mathlib.CategoryTheory.Sites.LocallyBijective
/-- A morphism of sheaves of types is locally bijective iff it is an isomorphism.
(This is generalized below as `isLocallyBijective_iff_isIso`.)  -/
_private.Mathlib.CategoryTheory.Sites.LocallyBijective.0.CategoryTheory.Sheaf.isLocallyBijective_iff_isIso' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  {F G : CategoryTheory.Sheaf J (Type w)} (f : F ⟶ G),
  CategoryTheory.Sheaf.IsLocallyInjective f ∧ CategoryTheory.Sheaf.IsLocallySurjective f ↔ CategoryTheory.IsIso f
-- Mathlib.Algebra.Group.Defs
mul_assoc : ∀ {G : Type u_1} [inst : Semigroup G] (a b c : G), a * b * c = a * (b * c)
-- Init.Data.List.Basic
_private.Init.Data.List.Basic.0.List.replicateTR.loop.match_1.eq_1 : ∀ {α : Type u_1} (motive : ℕ → List α → Sort u_2) (as : List α) (h_1 : (as : List α) → motive 0 as)
  (h_2 : (n : ℕ) → (as : List α) → motive n.succ as),
  (match 0, as with
    | 0, as => h_1 as
    | n.succ, as => h_2 n as) =
    h_1 as
-- Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
MeasureTheory.Measure.rnDeriv_mul_rnDeriv : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ ν κ : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ]
  [MeasureTheory.SigmaFinite ν] [MeasureTheory.SigmaFinite κ],
  μ.AbsolutelyContinuous ν → μ.rnDeriv ν * ν.rnDeriv κ =ᵐ[κ] μ.rnDeriv κ
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring
HomogeneousSubsemiring.instPartialOrder : {ι : Type u_1} →
  {σ : Type u_2} →
    {A : Type u_3} →
      [inst : AddMonoid ι] →
        [inst_1 : Semiring A] →
          [inst_2 : SetLike σ A] →
            [inst_3 : AddSubmonoidClass σ A] →
              {𝒜 : ι → σ} → [inst_4 : DecidableEq ι] → [inst_5 : GradedRing 𝒜] → PartialOrder (HomogeneousSubsemiring 𝒜)
-- Mathlib.Data.Set.Opposite
Set.opEquiv_apply : ∀ {α : Type u_1} (s : Set α), Set.opEquiv s = s.op
-- Mathlib.Algebra.Order.GroupWithZero.Basic
inv_lt_one_iff₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : LinearOrder G₀] {a : G₀} [PosMulStrictMono G₀]
  [ZeroLEOneClass G₀], a⁻¹ < 1 ↔ a ≤ 0 ∨ 1 < a
-- Mathlib.NumberTheory.EulerProduct.DirichletLSeries
/-- The Euler product for Dirichlet L-series, valid for `s.re > 1`.
This version is stated in terms of `tprod`.  -/
DirichletCharacter.LSeries_eulerProduct_tprod : ∀ {s : ℂ} {N : ℕ} (χ : DirichletCharacter ℂ N),
  1 < s.re → ∏' (p : Nat.Primes), (1 - χ ↑↑p * ↑↑p ^ (-s))⁻¹ = LSeries (fun n => χ ↑n) s
-- Lean.Parser.Do
Lean.Parser.Term.elseIf.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Probability.Process.Filtration
MeasureTheory.Filtration.le' : ∀ {Ω : Type u_1} {ι : Type u_2} [inst : Preorder ι] {m : MeasurableSpace Ω} (self : MeasureTheory.Filtration ι m)
  (i : ι), ↑self i ≤ m
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
CategoryTheory.Limits.prod.inr.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] (X Y : C)
  [inst_2 : CategoryTheory.Limits.HasBinaryProduct X Y],
  CategoryTheory.Limits.prod.inr X Y = CategoryTheory.Limits.prod.lift 0 (CategoryTheory.CategoryStruct.id Y)
-- Mathlib.Computability.PartrecBasis
Nat.Partrec'.of_prim : ∀ {n : ℕ} {f : List.Vector ℕ n → ℕ}, Primrec f → Nat.Partrec' ↑f
-- Mathlib.Algebra.Homology.AlternatingConst
ChainComplex.instHasHomologyNatObjAlternatingConst : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [CategoryTheory.Limits.HasZeroObject C] (X : C) (n : ℕ),
  HomologicalComplex.HasHomology (ChainComplex.alternatingConst.obj X) n
-- Init.Data.Array.Lemmas
Array.filterMap_filterMap : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → Option β} {g : β → Option γ} {xs : Array α},
  Array.filterMap g (Array.filterMap f xs) = Array.filterMap (fun x => (f x).bind g) xs
-- Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
/-- The `z`-derivative of the Jacobi theta function,
`θ' z τ = ∑' (n : ℤ), 2 * π * I * n * cexp (2 * π * I * n * z + π * I * n ^ 2 * τ)`.
 -/
jacobiTheta₂' : ℂ → ℂ → ℂ
-- Init.Control.State
instSubsingletonStateM : ∀ {σ α : Type u_1} [Subsingleton σ] [Subsingleton α], Subsingleton (StateM σ α)
-- Init.Data.SInt.Lemmas
Int32.ofBitVec_uInt32ToBitVec : ∀ (x : UInt32), Int32.ofBitVec x.toBitVec = x.toInt32
-- Mathlib.Analysis.Calculus.Deriv.Mul
/-- **Alias** of `HasStrictDerivAt.fun_finsetProd`. -/
HasStrictDerivAt.fun_finset_prod : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {ι : Type u_2} [inst_1 : DecidableEq ι] {𝔸' : Type u_3}
  [inst_2 : NormedCommRing 𝔸'] [inst_3 : NormedAlgebra 𝕜 𝔸'] {u : Finset ι} {f : ι → 𝕜 → 𝔸'} {f' : ι → 𝔸'},
  (∀ i ∈ u, HasStrictDerivAt (f i) (f' i) x) →
    HasStrictDerivAt (fun x => ∏ i ∈ u, f i x) (∑ i ∈ u, (∏ j ∈ u.erase i, f j x) • f' i) x
-- Init.Data.Int.DivMod.Bootstrap
Int.natCast_emod : ∀ (m n : ℕ), ↑(m % n) = ↑m % ↑n
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.awayMap_mk : ∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [inst : CommRing A] [inst_1 : SetLike σ A]
  [inst_2 : AddSubgroupClass σ A] [inst_3 : AddCommMonoid ι] [inst_4 : DecidableEq ι] (𝒜 : ι → σ)
  [inst_5 : GradedRing 𝒜] {e : ι} {f g : A} (hg : g ∈ 𝒜 e) {x : A} (hx : x = f * g) {d : ι} (n : ℕ) (hf : f ∈ 𝒜 d)
  (a : A) (ha : a ∈ 𝒜 (n • d)),
  (HomogeneousLocalization.awayMap 𝒜 hg hx) (HomogeneousLocalization.Away.mk 𝒜 hf n a ha) =
    HomogeneousLocalization.Away.mk 𝒜 ⋯ n (a * g ^ n) ⋯
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.compQuasiMeasurePreserving_id : ∀ {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace γ] [inst_1 : MeasurableSpace β] {ν : MeasureTheory.Measure β}
  (g : β →ₘ[ν] γ), g.compQuasiMeasurePreserving id ⋯ = g
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw.foldRevM_eq_foldrM_toListModel : ∀ {α : Type u} {β : α → Type v} {δ : Type w} {m : Type w → Type w'} [inst : Monad m] [LawfulMonad m]
  {f : δ → (a : α) → β a → m δ} {init : δ} {b : Std.DHashMap.Raw α β},
  Std.DHashMap.Raw.Internal.foldRevM f init b =
    List.foldrM (fun a b => f b a.fst a.snd) init (Std.DHashMap.Internal.toListModel b.buckets)
-- Init.Data.BitVec.Bitblast
BitVec.sle_eq_carry : ∀ {w : ℕ} {x y : BitVec w}, x.sle y = !(x.msb == y.msb ^^ BitVec.carry w y (~~~x) true)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
/-- If `X` represents a presheaf of monoids, then `X` is a monoid object.  -/
CategoryTheory.MonObj.ofRepresentableBy : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v, u_1} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      (X : C) →
        (F : CategoryTheory.Functor Cᵒᵖ MonCat) →
          (F.comp (CategoryTheory.forget MonCat)).RepresentableBy X → CategoryTheory.MonObj X
-- Mathlib.NumberTheory.NumberField.House
_private.Mathlib.NumberTheory.NumberField.House.0.NumberField.house.c.eq_1 : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] [inst_2 : DecidableEq (K →+* ℂ)],
  NumberField.house.c✝ K = ↑(Module.finrank ℚ K) * ‖(NumberField.basisMatrix K).transpose⁻¹‖
-- Mathlib.Analysis.InnerProductSpace.Adjoint
ContinuousLinearMap.adjoint_innerSL_apply : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : CompleteSpace E] (x : E),
  ContinuousLinearMap.adjoint ((innerSL 𝕜) x) = ContinuousLinearMap.toSpanSingleton 𝕜 x
-- Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite
Finset.prod_eq_prod_Ico_succ_bot : ∀ {M : Type u_2} [inst : CommMonoid M] {a b : ℕ},
  a < b → ∀ (f : ℕ → M), ∏ k ∈ Finset.Ico a b, f k = f a * ∏ k ∈ Finset.Ico (a + 1) b, f k
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Ideal.mul_inf : ∀ {A : Type u_2} [inst : CommRing A] [IsDedekindDomain A] (I J K : Ideal A), I * (J ⊓ K) = I * J ⊓ I * K
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalSubalgebra.inclusion_mk : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  {S T : NonUnitalSubalgebra R A} (h : S ≤ T) (x : A) (hx : x ∈ S), (NonUnitalSubalgebra.inclusion h) ⟨x, hx⟩ = ⟨x, ⋯⟩
-- Init.Data.Nat.Basic
Nat.sub_eq_of_eq_add : ∀ {a b c : ℕ}, a = c + b → a - b = c