mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Notation.Defs
dite_div : ∀ {α : Type u_2} (P : Prop) [inst : Decidable P] [inst_1 : Div α] (a : P → α) (b : ¬P → α) (c : α),
  (if h : P then a h else b h) / c = if h : P then a h / c else b h / c
-- Mathlib.NumberTheory.PellMatiyasevic
Pell.pell_eqz : ∀ {a : ℕ} (a1 : 1 < a) (n : ℕ), Pell.xz a1 n * Pell.xz a1 n - ↑(Pell.d✝ a1) * Pell.yz a1 n * Pell.yz a1 n = 1
-- Mathlib.Data.Subtype
Subtype.coe_prop : ∀ {α : Type u_1} {S : Set α} (a : { a // a ∈ S }), ↑a ∈ S
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.instIsZeroApplySet : ∀ {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M],
  IsZeroApply (MeasureTheory.VectorMeasure α M) (Set α) M
-- Lean.Expr
Lean.Expr.getRevArg! : Lean.Expr → ℕ → Lean.Expr
-- Mathlib.Analysis.LocallyConvex.Bounded
Bornology.isVonNBounded_sub : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] [ContinuousSMul 𝕜 E] [IsTopologicalAddGroup E] {s t : Set E},
  Bornology.IsVonNBounded 𝕜 (s - t) ↔ s = ∅ ∨ t = ∅ ∨ Bornology.IsVonNBounded 𝕜 s ∧ Bornology.IsVonNBounded 𝕜 t
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
Mathlib.Tactic.BicategoryLike.HorizontalComp.brecOn.eq : ∀ {motive : Mathlib.Tactic.BicategoryLike.HorizontalComp → Sort u} (t : Mathlib.Tactic.BicategoryLike.HorizontalComp)
  (F_1 :
    (t : Mathlib.Tactic.BicategoryLike.HorizontalComp) →
      Mathlib.Tactic.BicategoryLike.HorizontalComp.below t → motive t),
  Mathlib.Tactic.BicategoryLike.HorizontalComp.brecOn t F_1 =
    F_1 t (Mathlib.Tactic.BicategoryLike.HorizontalComp.brecOn.go t F_1).2
-- Mathlib.Topology.UniformSpace.Cauchy
Filter.TotallyBounded.exists_clusterPt : ∀ {α : Type u} [uniformSpace : UniformSpace α] [CompleteSpace α] {f : Filter α} [f.NeBot],
  f.TotallyBounded → ∃ x, ClusterPt x f
-- Init.Grind.Ring.CommSemiringAdapter
Lean.Grind.CommRing.Poly.denoteS_mulConst : ∀ {α : Type u_1} [inst : Lean.Grind.Semiring α] (ctx : Lean.Grind.CommRing.Context α) (k : ℤ)
  (p : Lean.Grind.CommRing.Poly),
  k ≥ 0 →
    p.NonnegCoeffs →
      Lean.Grind.CommRing.Poly.denoteS ctx (Lean.Grind.CommRing.Poly.mulConst k p) =
        ↑k.toNat * Lean.Grind.CommRing.Poly.denoteS ctx p
-- Mathlib.Analysis.Calculus.FDeriv.Measurable
measurable_deriv_with_param : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_3} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {α : Type u_4} [inst_3 : TopologicalSpace α] [inst_4 : MeasurableSpace α]
  [OpensMeasurableSpace α] [CompleteSpace F] [LocallyCompactSpace 𝕜] [inst_8 : MeasurableSpace 𝕜]
  [OpensMeasurableSpace 𝕜] [inst_10 : MeasurableSpace F] [BorelSpace F] {f : α → 𝕜 → F},
  Continuous (Function.uncurry f) → Measurable fun p => deriv (f p.1) p.2
-- Mathlib.Order.RelClasses
WellFoundedGT.fix.eq_1 : ∀ {α : Type u} [inst : LT α] [inst_1 : WellFoundedGT α] {motive : α → Sort u_1},
  WellFoundedGT.fix = IsWellFounded.fix fun x1 x2 => x2 < x1
-- Mathlib.Order.Interval.Basic
Interval.pure_injective : ∀ {α : Type u_1} [inst : Preorder α], Function.Injective Interval.pure
-- Std.Data.DHashMap.Internal.RawLemmas
/-- Variant of `getD_map` that holds with `EquivBEq` (i.e. without `LawfulBEq`).  -/
Std.DHashMap.Internal.Raw₀.Const.getD_map' : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {γ : Type w}
  (m : Std.DHashMap.Internal.Raw₀ α fun x => β) [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] {f : α → β → γ}
  {k : α} {fallback : γ} (h : (↑m).WF),
  Std.DHashMap.Internal.Raw₀.Const.getD (Std.DHashMap.Internal.Raw₀.map f m) k fallback =
    (Option.pmap (fun v h => f (m.getKey k h) v) (Std.DHashMap.Internal.Raw₀.Const.get? m k) ⋯).getD fallback
-- Lean.Meta.AppBuilder
/-- Returns `a + b` using a heterogeneous `+`. This method assumes `a` and `b` have the same type.  -/
Lean.Meta.mkAdd : Lean.Expr → Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Topology.Closure
/-- **Alias** of the reverse direction of `dense_closure`.

---

The closure of a set `s` is dense if and only if `s` is dense.  -/
Dense.closure : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, Dense s → Dense (closure s)
-- Mathlib.Data.Setoid.Partition
/-- A family of injective functions with pairwise disjoint
domains and pairwise disjoint ranges can be glued together
to form an injective function.  -/
IndexedPartition.piecewise_inj : ∀ {ι : Type u_1} {α : Type u_2} {s : ι → Set α} (hs : IndexedPartition s) {β : Type u_3} {f : ι → α → β},
  (∀ (i : ι), Set.InjOn (f i) (s i)) →
    (Set.univ.PairwiseDisjoint fun i => f i '' s i) → Function.Injective (hs.piecewise f)
-- Mathlib.CategoryTheory.Limits.Cones
/-- Functorially associated to each functor `J ⥤ C`, we have the `C`-presheaf consisting of
cones with a given cone point.
 -/
CategoryTheory.cones : (J : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    (C : Type u₃) →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        CategoryTheory.Functor (CategoryTheory.Functor J C) (CategoryTheory.Functor Cᵒᵖ (Type (max u₁ v₃)))
-- Mathlib.Topology.UniformSpace.Completion
UniformSpace.Completion.map_id : ∀ {α : Type u_1} [inst : UniformSpace α], UniformSpace.Completion.map id = id
-- Mathlib.Data.List.Sublists
_private.Mathlib.Data.List.Sublists.0.List.sublistsLenAux.match_1.eq_3 : ∀ {α : Type u_1} {β : Type u_2} (motive : ℕ → List α → (List α → β) → List β → Sort u_3) (n : ℕ) (a : α) (l : List α)
  (f : List α → β) (r : List β) (h_1 : (x : List α) → (f : List α → β) → (r : List β) → motive 0 x f r)
  (h_2 : (n : ℕ) → (x : List α → β) → (r : List β) → motive n.succ [] x r)
  (h_3 : (n : ℕ) → (a : α) → (l : List α) → (f : List α → β) → (r : List β) → motive n.succ (a :: l) f r),
  (match n.succ, a :: l, f, r with
    | 0, x, f, r => h_1 x f r
    | n.succ, [], x, r => h_2 n x r
    | n.succ, a :: l, f, r => h_3 n a l f r) =
    h_3 n a l f r
-- Mathlib.Algebra.Group.Commute.Basic
AddCommute.self_zsmul : ∀ {G : Type u_1} [inst : AddGroup G] (a : G) (n : ℤ), AddCommute a (n • a)
-- Mathlib.Analysis.InnerProductSpace.NormDet
/-- The square of `f.normDet` equals the determinant of `f.adjoint ∘L f`.
 -/
ContinuousLinearMap.normDet_sq : ∀ {𝕜 : Type u_1} {U : Type u_2} {V : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup U]
  [inst_2 : InnerProductSpace 𝕜 U] [inst_3 : FiniteDimensional 𝕜 U] [inst_4 : NormedAddCommGroup V]
  [inst_5 : InnerProductSpace 𝕜 V] [inst_6 : CompleteSpace V] (f : U →L[𝕜] V),
  ↑((↑f).normDet ^ 2) = (ContinuousLinearMap.adjoint f ∘SL f).det
-- Mathlib.Data.Finsupp.MonomialOrder
MonomialOrder.toSyn_lt_iff_ne_zero : ∀ {σ : Type u_1} (m : MonomialOrder σ) {a : m.syn}, 0 < a ↔ a ≠ 0
-- Mathlib.Algebra.Category.Ring.Colimits
RingCat.Colimits.Relation.below.add_2 : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J RingCat}
  {motive : (a a_1 : RingCat.Colimits.Prequotient F) → RingCat.Colimits.Relation F a a_1 → Prop}
  (x y y' : RingCat.Colimits.Prequotient F) (x_1 : RingCat.Colimits.Relation F y y'),
  RingCat.Colimits.Relation.below x_1 → motive y y' x_1 → RingCat.Colimits.Relation.below ⋯
-- Mathlib.ModelTheory.Bundled
FirstOrder.Language.Theory.ModelType.instInhabited : {L : FirstOrder.Language} → Inhabited ∅.ModelType
-- Mathlib.Algebra.Homology.DerivedCategory.Plus
DerivedCategory.Plus.instAdditiveSingleFunctor : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] (n : ℤ), (DerivedCategory.Plus.singleFunctor C n).Additive
-- Mathlib.Order.GaloisConnection.Basic
GaloisInsertion.l_biSup_u : ∀ {α : Type u} {β : Type v} {l : α → β} {u : β → α} [inst : CompleteLattice α] [inst_1 : CompleteLattice β]
  (gi : GaloisInsertion l u) {ι : Sort x} {p : ι → Prop} (f : (i : ι) → p i → β),
  l (⨆ i, ⨆ (hi : p i), u (f i hi)) = ⨆ i, ⨆ (hi : p i), f i hi
-- Mathlib.LinearAlgebra.RootSystem.Chain
/-- **Alias** of `RootPairing.setOfPred_root_sub_zsmul_mem_eq_Icc`. -/
RootPairing.setOf_root_sub_zsmul_mem_eq_Icc : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Finite ι] [inst_1 : CommRing R]
  [inst_2 : CharZero R] [inst_3 : IsDomain R] [inst_4 : AddCommGroup M] [inst_5 : Module R M] [inst_6 : AddCommGroup N]
  [inst_7 : Module R N] {P : RootPairing ι R M N} [inst_8 : P.IsCrystallographic] {i j : ι},
  LinearIndependent R ![P.root i, P.root j] →
    {k | P.root j - k • P.root i ∈ Set.range ⇑P.root} =
      Set.Icc (-↑(RootPairing.chainTopCoeff i j)) ↑(RootPairing.chainBotCoeff i j)
-- Mathlib.Algebra.Lie.Basic
/-- A Lie algebra bracket is compatible with scalar multiplication in its second argument.

The compatibility in the first argument is not a class property, but follows since every
Lie algebra has a natural Lie module action on itself, see `LieModule`.  -/
LieAlgebra.lie_smul : ∀ {R : Type u} {L : Type v} {inst : CommRing R} {inst_1 : LieRing L} [self : LieAlgebra R L] (t : R) (x y : L),
  ⁅x, t • y⁆ = t • ⁅x, y⁆
-- Mathlib.CategoryTheory.Adjunction.Evaluation
/-- The right adjoint of evaluation.  -/
CategoryTheory.evaluationRightAdjoint : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (D : Type u₂) →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        [∀ (a b : C), CategoryTheory.Limits.HasProductsOfShape (a ⟶ b) D] →
          C → CategoryTheory.Functor D (CategoryTheory.Functor C D)
-- Mathlib.Analysis.SpecialFunctions.Complex.Log
Complex.log_neg_one : Complex.log (-1) = ↑Real.pi * Complex.I
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
MeasureTheory.aecover_Ioc_of_Ico : ∀ {α : Type u_1} {ι : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {l : Filter ι}
  [inst_1 : LinearOrder α] [inst_2 : TopologicalSpace α] [OrderClosedTopology α] [OpensMeasurableSpace α] {a b : ι → α}
  {A B : α} [MeasureTheory.NullSingletonClass μ],
  Filter.Tendsto a l (nhds A) →
    Filter.Tendsto b l (nhds B) → MeasureTheory.AECover (μ.restrict (Set.Ioc A B)) l fun i => Set.Ico (a i) (b i)
-- Mathlib.Algebra.Group.InjSurj
Function.Injective.invOneClass.eq_1 : ∀ {M₁ : Type u_1} {M₂ : Type u_2} [inst : One M₁] [inst_1 : Inv M₁] [inst_2 : InvOneClass M₂] (f : M₁ → M₂)
  (hf : Function.Injective f) (one : f 1 = 1) (inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹),
  Function.Injective.invOneClass f hf one inv = { toOne := inst, toInv := inst_1, inv_one := ⋯ }
-- Mathlib.Tactic.Peel
Mathlib.Tactic.Peel.frequently_congr : ∀ {α : Type u_1} {p q : α → Prop} {f : Filter α},
  (∀ (x : α), p x ↔ q x) → ((∃ᶠ (x : α) in f, p x) ↔ ∃ᶠ (x : α) in f, q x)
-- Mathlib.CategoryTheory.RepresentedBy
CategoryTheory.Functor.IsRepresentedBy.iff_exists_representableBy : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C}
  {x : F.obj (Opposite.op X)}, F.IsRepresentedBy x ↔ ∃ R, R.homEquiv (CategoryTheory.CategoryStruct.id X) = x
-- Mathlib.RingTheory.Idempotents
/-- A complete orthogonal family of central idempotents in a semiring
give rise to a direct product decomposition.  -/
CompleteOrthogonalIdempotents.ringEquivOfIsMulCentral : {R : Type u_1} →
  {I : Type u_2} →
    [inst : Fintype I] →
      {e : I → R} →
        [inst_1 : Semiring R] →
          (he : CompleteOrthogonalIdempotents e) → (∀ (i : I), IsMulCentral (e i)) → R ≃+* ((i : I) → ⋯.Corner)
-- Batteries.Data.BitVec.Lemmas
BitVec.toNat_pow : ∀ {w : ℕ} (b : BitVec w) (n : ℕ), (b ^ n).toNat = b.toNat ^ n % 2 ^ w
-- Mathlib.RingTheory.LocalRing.ResidueField.Ideal
/-- If `I = f⁻¹(J)`, then there is a canonical embedding `κ(I) ↪ κ(J)`.  -/
Ideal.ResidueField.mapₐ : {R : Type u_1} →
  {A : Type u_3} →
    {B : Type u_4} →
      [inst : CommRing R] →
        [inst_1 : CommRing A] →
          [inst_2 : CommRing B] →
            [inst_3 : Algebra R A] →
              [inst_4 : Algebra R B] →
                (I : Ideal A) →
                  [inst_5 : I.IsPrime] →
                    (J : Ideal B) →
                      [inst_6 : J.IsPrime] →
                        (f : A →ₐ[R] B) → I = Ideal.comap f.toRingHom J → I.ResidueField →ₐ[R] J.ResidueField
-- Std.Data.DTreeMap.Basic
/-- Tries to retrieve the largest key that is less than the given key,
returning `fallback` if no such key exists.
 -/
Std.DTreeMap.getKeyLTD : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → Std.DTreeMap α β cmp → α → α → α
-- Mathlib.Data.Num.ZNum
Num.gcdAux.eq_3 : ∀ (x x_1 : Num) (n : ℕ), (x = Num.zero → False) → Num.gcdAux n.succ x x_1 = Num.gcdAux n (x_1 % x) x
-- Init.Data.SInt.Lemmas
Int32.lt_of_le_of_lt : ∀ {a b c : Int32}, a ≤ b → b < c → a < c
-- Mathlib.Topology.Spectral.Basic
SpectralSpace.toCompactSpace : ∀ {X : Type u_3} {inst : TopologicalSpace X} [self : SpectralSpace X], CompactSpace X
-- Mathlib.MeasureTheory.SetSemiring
/-- In a semiring of sets `C`, for all set `s ∈ C` and finite set of sets `I ⊆ C`, there is a
finite set of sets in `C` whose union is `s \ ⋃₀ I`.
See `IsSetSemiring.disjointOfDiffUnion` for a definition that gives such a set.  -/
MeasureTheory.IsSetSemiring.exists_disjoint_finset_sdiff_eq : ∀ {α : Type u_1} {C : Set (Set α)} {s : Set α} {I : Finset (Set α)},
  MeasureTheory.IsSetSemiring C → s ∈ C → ↑I ⊆ C → ∃ J, ↑J ⊆ C ∧ (↑J).PairwiseDisjoint id ∧ s \ ⋃₀ ↑I = ⋃₀ ↑J
-- Mathlib.GroupTheory.PresentedGroup
/-- The extension of a map `f : α → G` that satisfies the given relations to a group homomorphism
from `PresentedGroup rels → G`.  -/
PresentedGroup.toGroup : {α : Type u_1} →
  {G : Type u_3} →
    [inst : Group G] →
      {f : α → G} → {rels : Set (FreeGroup α)} → (∀ r ∈ rels, (FreeGroup.lift f) r = 1) → PresentedGroup rels →* G
-- Mathlib.Topology.Category.CompHaus.Projective
CompHaus.instEnoughProjectives : CategoryTheory.EnoughProjectives CompHaus
-- Lean.Meta.Match.MatchEqsExt
Lean.Meta.Match.MatchEqns : Type
-- Mathlib.Order.Interval.Set.Fin
Fin.preimage_natAdd_Ici_natAdd : ∀ {n : ℕ} (m : ℕ) (i : Fin n), Fin.natAdd m ⁻¹' Set.Ici (Fin.natAdd m i) = Set.Ici i
-- Mathlib.Data.TypeVec
TypeVec.id.eq_1 : ∀ {n : ℕ} {α : TypeVec.{u_1} n} (x : Fin2 n) (x_1 : α x), TypeVec.id x x_1 = x_1
-- Mathlib.Data.Set.Sups
Set.subset_infs_self : ∀ {α : Type u_2} [inst : SemilatticeInf α] {s : Set α}, s ⊆ s ⊼ s
-- Mathlib.Algebra.Category.Grp.Limits
CommGrpCat.forget_createsLimitsOfSize.eq_1 : CommGrpCat.forget_createsLimitsOfSize =
  { CreatesLimitsOfShape := fun {J} [CategoryTheory.Category.{w, v} J] => inferInstance }
-- Mathlib.Analysis.Convex.Segment
segment_subset_Icc : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : PartialOrder E] [IsOrderedAddMonoid E] [inst_5 : Module 𝕜 E] [PosSMulMono 𝕜 E] {x y : E},
  x ≤ y → segment 𝕜 x y ⊆ Set.Icc x y
-- Mathlib.Topology.Homotopy.Basic
/-- Given a `HomotopyWith f₀ f₁ P`, we can define a `HomotopyWith f₁ f₀ P` by reversing the homotopy.
 -/
ContinuousMap.HomotopyWith.symm : {X : Type u} →
  {Y : Type v} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] →
        {P : C(X, Y) → Prop} → {f₀ f₁ : C(X, Y)} → f₀.HomotopyWith f₁ P → f₁.HomotopyWith f₀ P
-- Mathlib.Algebra.Order.Archimedean.Basic
instArchimedeanInt : Archimedean ℤ
-- Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
/-- The set `{ y : R | v y = v x }` is a neighbourhood of `x`.
This does not imply that `v` is locally constant everywhere (since `v ⁻¹' {0}` is not open),
but it is equivalent to the restriction of `v` to the complement of its support being
locally constant.  -/
Valuation.locally_const : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : ValuativeRel R] {Γ₀ : Type u_3} [inst_2 : LinearOrderedCommGroupWithZero Γ₀]
  [inst_3 : TopologicalSpace R] (v : Valuation R Γ₀) [v.Compatible] [IsValuativeTopology R] {x : R},
  v x ≠ 0 → {y | v y = v x} ∈ nhds x
-- Std.Sat.AIG.RefVec
Std.Sat.AIG.BinaryRefVec.rhs : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] → {aig : Std.Sat.AIG α} → {len : ℕ} → aig.BinaryRefVec len → aig.RefVec len
-- Mathlib.LinearAlgebra.Dimension.StrongRankCondition
/-- If a vector space (or module) has a finite basis, then its dimension (or rank) is equal to the
cardinality of the basis. This lemma uses a `Finset` instead of indexed types.  -/
Module.finrank_eq_card_finset_basis : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [StrongRankCondition R]
  {ι : Type w} {b : Finset ι} (h : Module.Basis (↥b) R M), Module.finrank R M = b.card
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.monomial_one_mul_cancel_left_iff : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {p q : MvPolynomial σ R} {m : σ →₀ ℕ},
  (MvPolynomial.monomial m) 1 * p = (MvPolynomial.monomial m) 1 * q ↔ p = q
-- Mathlib.SetTheory.Cardinal.Regular
Cardinal.isRegular_succ : ∀ {c : Cardinal.{u_1}}, Cardinal.aleph0 ≤ c → (Order.succ c).IsRegular
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.instDistrib : {d : ℤ} → Distrib (ℤ√d)
-- Mathlib.Algebra.Order.Star.Basic
instIsStrictOrderedModuleOfIsCancelAdd : ∀ {R : Type u_1} {A : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R] [StarOrderedRing R]
  [inst_4 : NonUnitalSemiring A] [inst_5 : StarRing A] [inst_6 : PartialOrder A] [StarOrderedRing A]
  [inst_8 : Module R A] [StarModule R A] [IsScalarTower R A A] [SMulCommClass R A A] [IsDomain R] [IsCancelAdd A]
  [Module.IsTorsionFree R A] [IsCancelAdd R], IsStrictOrderedModule R A
-- Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
WeierstrassCurve.hasSplitMultiplicativeReduction_iff : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsDiscreteValuationRing R] {K : Type u_2}
  [inst_3 : Field K] [inst_4 : Algebra R K] [inst_5 : IsFractionRing R K] (W : WeierstrassCurve K),
  WeierstrassCurve.HasSplitMultiplicativeReduction R W ↔
    ∃ (toHasMultiplicativeReduction : WeierstrassCurve.HasMultiplicativeReduction R W),
      (Polynomial.map (algebraMap R (IsLocalRing.ResidueField R))
          (Polynomial.C (WeierstrassCurve.integralModel R W).c₄ * Polynomial.X ^ 2 +
              Polynomial.C ((WeierstrassCurve.integralModel R W).a₁ * (WeierstrassCurve.integralModel R W).c₄) *
                Polynomial.X -
            Polynomial.C
              (54 * (WeierstrassCurve.integralModel R W).b₆ -
                  3 * (WeierstrassCurve.integralModel R W).b₂ * (WeierstrassCurve.integralModel R W).b₄ +
                (WeierstrassCurve.integralModel R W).a₂ * (WeierstrassCurve.integralModel R W).c₄))).Splits
-- Init.SimpLemmas
implies_congr_ctx : ∀ {p₁ p₂ q₁ q₂ : Prop}, p₁ = p₂ → (p₂ → q₁ = q₂) → (p₁ → q₁) = (p₂ → q₂)
-- Init.Data.Float.Model.Float32
Float32.Model.instMin : Min Float32.Model
-- Init.Data.Int.Linear
Int.Internal.Linear.mul_eq_kkx : ∀ (a b k₁ k₂ c k : ℤ), a = k₁ → b = k₂ * c → (k₁ * k₂ == k) = true → a * b = k * c
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.piecewise_source : ∀ {α : Type u_1} {β : Type u_2} (e e' : PartialEquiv α β) (s : Set α) (t : Set β) [inst : (x : α) → Decidable (x ∈ s)]
  [inst_1 : (y : β) → Decidable (y ∈ t)] (H : e.IsImage s t) (H' : e'.IsImage s t),
  (e.piecewise e' s t H H').source = s.ite e.source e'.source
-- Lean.Meta.DecLevel
Lean.Meta.decLevel : Lean.Level → Lean.MetaM Lean.Level
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.Red.Step.diamond : ∀ {α : Type u} {L₁ L₂ L₃ L₄ : List (α × Bool)},
  FreeAddGroup.Red.Step L₁ L₃ →
    FreeAddGroup.Red.Step L₂ L₄ → L₁ = L₂ → L₃ = L₄ ∨ ∃ L₅, FreeAddGroup.Red.Step L₃ L₅ ∧ FreeAddGroup.Red.Step L₄ L₅
-- Mathlib.NumberTheory.LSeries.Basic
LSeries.term_def : ∀ (f : ℕ → ℂ) (s : ℂ) (n : ℕ), LSeries.term f s n = if n = 0 then 0 else f n / ↑n ^ s
-- Mathlib.CategoryTheory.ConcreteCategory.Forget
/-- In order to construct a “partially forgetting” functor, we do not need to verify functor laws;
it suffices to ensure that compositions agree with `forget₂ C D ⋙ forget D = forget C`.
 -/
CategoryTheory.HasForget₂.mk' : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {FC : outParam (C → C → Type u_2)} →
      {CC : outParam (C → Type w)} →
        [inst_1 : outParam ((X Y : C) → FunLike (FC X Y) (CC X) (CC Y))] →
          [inst_2 : CategoryTheory.ConcreteCategory C FC] →
            {D : Type u_3} →
              [inst_3 : CategoryTheory.Category.{v_2, u_3} D] →
                {FD : outParam (D → D → Type u_4)} →
                  {CD : outParam (D → Type w)} →
                    [inst_4 : outParam ((X Y : D) → FunLike (FD X Y) (CD X) (CD Y))] →
                      [inst_5 : CategoryTheory.ConcreteCategory D FD] →
                        (obj : C → D) →
                          (∀ (X : C), (CategoryTheory.forget D).obj (obj X) = (CategoryTheory.forget C).obj X) →
                            (map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)) →
                              (∀ {X Y : C} {f : X ⟶ Y},
                                  (CategoryTheory.forget D).map (map f) ≍ (CategoryTheory.forget C).map f) →
                                CategoryTheory.HasForget₂ C D
-- Mathlib.Combinatorics.Young.YoungDiagram
YoungDiagram.mem_col_iff : ∀ {μ : YoungDiagram} {j : ℕ} {c : ℕ × ℕ}, c ∈ μ.col j ↔ c ∈ μ ∧ c.2 = j
-- Std.Data.HashSet.Lemmas
Std.HashSet.Equiv.get_eq : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {k : α} (hk : k ∈ m₁) (h : m₁.Equiv m₂), m₁.get k hk = m₂.get k ⋯
-- Mathlib.Order.CompleteBooleanAlgebra
disjoint_iSup₂_iff : ∀ {α : Type u} {ι : Sort w} {κ : ι → Sort w'} [inst : Order.Frame α] {a : α} {f : (i : ι) → κ i → α},
  Disjoint a (⨆ i, ⨆ j, f i j) ↔ ∀ (i : ι) (j : κ i), Disjoint a (f i j)
-- Mathlib.Analysis.SpecialFunctions.Exp
Real.comap_exp_nhds_exp : ∀ (x : ℝ), Filter.comap Real.exp (nhds (Real.exp x)) = nhds x
-- Init.Data.Iterators.Consumers.Collect
/-- Traverses the given iterator and stores the emitted values in an array.

This function is deprecated. Instead of `it.allowNontermination.toArray`, use `it.toArray`.
 -/
Std.Iter.Partial.toArray : {α β : Type w} → [Std.Iterator α Id β] → Std.Iter.Partial β → Array β
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.instIsCentralScalar : ∀ {α : Type u_1} [inst : TopologicalSpace α] {R : Type u_3} {M : Type u_5} [inst_1 : TopologicalSpace M]
  [inst_2 : SMul R M] [inst_3 : SMul Rᵐᵒᵖ M] [inst_4 : ContinuousConstSMul R M] [inst_5 : IsCentralScalar R M],
  IsCentralScalar R C(α, M)
-- Mathlib.Algebra.Order.GroupWithZero.Basic
pow_succ_pos : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] [inst_1 : PartialOrder M₀] {a : M₀} [PosMulStrictMono M₀],
  0 < a → ∀ (n : ℕ), 0 < a ^ (n + 1)
-- Mathlib.CategoryTheory.Sites.Coherent.SheafComparison
CategoryTheory.Presheaf.isSheaf_coherent_of_hasPullbacks_comp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {A : Type u₃}
  [inst_1 : CategoryTheory.Category.{v₃, u₃} A] (F : CategoryTheory.Functor Cᵒᵖ A) {B : Type u₄}
  [inst_2 : CategoryTheory.Category.{v₄, u₄} B] (s : CategoryTheory.Functor A B) [inst_3 : CategoryTheory.Preregular C]
  [inst_4 : CategoryTheory.FinitaryExtensive C]
  [h : ∀ {Y X : C} (f : Y ⟶ X) [CategoryTheory.EffectiveEpi f], CategoryTheory.Limits.HasPullback f f]
  [CategoryTheory.Limits.PreservesFiniteLimits s],
  CategoryTheory.Presheaf.IsSheaf (CategoryTheory.coherentTopology C) F →
    CategoryTheory.Presheaf.IsSheaf (CategoryTheory.coherentTopology C) (F.comp s)
-- Std.Data.DTreeMap.Internal.Cell
/-- Internal implementation detail of the tree map  -/
Std.DTreeMap.Internal.Cell.Const.get? : {α : Type u} →
  {β : Type v} → [inst : Ord α] → {k : α} → Std.DTreeMap.Internal.Cell α (fun x => β) (compare k) → Option β
-- Mathlib.Algebra.FreeMonoid.Basic
FreeMonoid.ofList.eq_1 : ∀ {α : Type u_1}, FreeMonoid.ofList = Equiv.refl (List α)
-- Mathlib.CategoryTheory.Preadditive.Basic
/-- Map any equalizer fork to a cone on the difference of the two morphisms.  -/
CategoryTheory.Preadditive.kernelForkOfFork : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {X Y : C} → {f g : X ⟶ Y} → CategoryTheory.Limits.Fork f g → CategoryTheory.Limits.KernelFork (f - g)