mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.BigOperators.ModEq
Nat.ModEq.listSum_zero : ∀ {n : ℕ} {l : List ℕ}, (∀ x ∈ l, x ≡ 0 [MOD n]) → l.sum ≡ 0 [MOD n]
-- Mathlib.Analysis.Normed.Module.Ball.Pointwise
ball_add_ball : ∀ {E : Type u_2} [inst : SeminormedAddCommGroup E] [NormedSpace ℝ E] {δ ε : ℝ},
  0 < ε → 0 < δ → ∀ (a b : E), Metric.ball a ε + Metric.ball b δ = Metric.ball (a + b) (ε + δ)
-- Mathlib.Probability.Kernel.Basic
ProbabilityTheory.Kernel.lintegral_piecewise : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ η : ProbabilityTheory.Kernel α β}
  {s : Set α} {hs : MeasurableSet s} [inst : DecidablePred fun x => x ∈ s] (a : α) (g : β → ENNReal),
  ∫⁻ (b : β), g b ∂(ProbabilityTheory.Kernel.piecewise hs κ η) a =
    if a ∈ s then ∫⁻ (b : β), g b ∂κ a else ∫⁻ (b : β), g b ∂η a
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.CanonArgKey.i : Lean.Meta.Grind.CanonArgKey → ℕ
-- Mathlib.CategoryTheory.Monad.Basic
CategoryTheory.Comonad.id_δ_app : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (X : C),
  (CategoryTheory.Comonad.id C).δ.app X = CategoryTheory.CategoryStruct.id X
-- Mathlib.Dynamics.Ergodic.Action.OfMinimal
aeconst_of_dense_setOfPred_preimage_vadd_eq : ∀ {M : Type u_1} [inst : TopologicalSpace M] {X : Type u_2} [inst_1 : TopologicalSpace X] [R1Space X]
  [inst_3 : MeasurableSpace X] [BorelSpace X] [inst_5 : VAdd M X] [ContinuousVAdd M X] {μ : MeasureTheory.Measure X}
  [MeasureTheory.IsFiniteMeasure μ] [μ.InnerRegular] [ErgodicVAdd M X μ] {s : Set X},
  MeasureTheory.NullMeasurableSet s μ →
    Dense {g | (fun x => g +ᵥ x) ⁻¹' s = s} → Filter.EventuallyConst s (MeasureTheory.ae μ)
-- Mathlib.Order.SuccPred.Limit
SuccOrder.limitRecOn_succ_of_not_isMax : ∀ {α : Type u_1} {b : α} {motive : α → Sort u_2} [inst : LinearOrder α] [inst_1 : SuccOrder α]
  [inst_2 : WellFoundedLT α] (isMin : (a : α) → IsMin a → motive a)
  (succ : (a : α) → ¬IsMax a → motive a → motive (Order.succ a))
  (isSuccLimit : (a : α) → Order.IsSuccLimit a → ((b : α) → b < a → motive b) → motive a) (hb : ¬IsMax b),
  SuccOrder.limitRecOn (Order.succ b) isMin succ isSuccLimit = succ b hb (SuccOrder.limitRecOn b isMin succ isSuccLimit)
-- Mathlib.Algebra.Order.Hom.Ring
OrderRingHom.coe_orderAddMonoidHom_id : ∀ {α : Type u_2} [inst : NonAssocSemiring α] [inst_1 : Preorder α], ↑(OrderRingHom.id α) = OrderAddMonoidHom.id α
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getD_emptyWithCapacity : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {a : α} {fallback : β} {c : ℕ},
  (Std.HashMap.Raw.emptyWithCapacity c).getD a fallback = fallback
-- Mathlib.Computability.NFA
NFA.evalFrom.eq_1 : ∀ {α : Type u} {σ : Type v} (M : NFA α σ) (S : Set σ), M.evalFrom S = List.foldl M.stepSet S
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
/-- The products of two functions `f g : ι → M` over finite sets `s₁ s₂ : Finset ι`
are equal if the functions agree on `s₁ ∩ s₂`, `f = 1` and `g = 1` on the respective
set differences.  -/
Finset.prod_congr_of_eq_on_inter : ∀ {ι : Type u_5} {M : Type u_6} {s₁ s₂ : Finset ι} {f g : ι → M} [inst : CommMonoid M],
  (∀ a ∈ s₁, a ∉ s₂ → f a = 1) →
    (∀ a ∈ s₂, a ∉ s₁ → g a = 1) → (∀ a ∈ s₁, a ∈ s₂ → f a = g a) → ∏ a ∈ s₁, f a = ∏ a ∈ s₂, g a
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarAlgebra.adjoin_induction : ∀ (R : Type u) {A : Type v} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : NonUnitalSemiring A]
  [inst_3 : StarRing A] [inst_4 : Module R A] [inst_5 : IsScalarTower R A A] [inst_6 : SMulCommClass R A A]
  [inst_7 : StarModule R A] {s : Set A} {p : (x : A) → x ∈ NonUnitalStarAlgebra.adjoin R s → Prop},
  (∀ (x : A) (hx : x ∈ s), p x ⋯) →
    (∀ (x y : A) (hx : x ∈ NonUnitalStarAlgebra.adjoin R s) (hy : y ∈ NonUnitalStarAlgebra.adjoin R s),
        p x hx → p y hy → p (x + y) ⋯) →
      p 0 ⋯ →
        (∀ (x y : A) (hx : x ∈ NonUnitalStarAlgebra.adjoin R s) (hy : y ∈ NonUnitalStarAlgebra.adjoin R s),
            p x hx → p y hy → p (x * y) ⋯) →
          (∀ (r : R) (x : A) (hx : x ∈ NonUnitalStarAlgebra.adjoin R s), p x hx → p (r • x) ⋯) →
            (∀ (x : A) (hx : x ∈ NonUnitalStarAlgebra.adjoin R s), p x hx → p (star x) ⋯) →
              ∀ {a : A} (ha : a ∈ NonUnitalStarAlgebra.adjoin R s), p a ha
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.closedUnder_univ : ∀ (L : FirstOrder.Language) {M : Type w} [inst : L.Structure M] {n : ℕ} (f : L.Functions n),
  FirstOrder.Language.ClosedUnder f Set.univ
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.isEmpty_diff_iff : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  (h₁ : m₁.WF),
  m₂.WF →
    ((m₁.diff m₂ ⋯).isEmpty = true ↔
      ∀ (k : α), Std.DTreeMap.Internal.Impl.contains k m₁ = true → Std.DTreeMap.Internal.Impl.contains k m₂ = true)
-- Mathlib.Algebra.GCDMonoid.Basic
gcd_zero_right : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] (a : α), gcd a 0 = normalize a
-- Mathlib.Geometry.Manifold.VectorBundle.Riemannian
_private.Mathlib.Geometry.Manifold.VectorBundle.Riemannian.0.«term⟪_,_⟫» : Lean.ParserDescr
-- Mathlib.Topology.MetricSpace.DilationEquiv
DilationEquiv.self_trans_symm : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] (e : X ≃ᵈ Y),
  e.trans e.symm = DilationEquiv.refl X
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.mul_zero : ∀ {m : Type u_1} {n : Type u_2} {A : Type u_5} {o : Type u_7} [inst : Fintype n] [inst_1 : NonUnitalNonAssocSemiring A]
  (M : CStarMatrix m n A), M * 0 = 0
-- Mathlib.RingTheory.HahnSeries.HahnEmbedding
/-- **Hahn embedding theorem**

For a linearly ordered additive group `M`, there exists an injective `OrderAddMonoidHom` from `M` to
`Lex ℝ⟦FiniteArchimedeanClass M⟧` that sends each `a : M` to an element of the `a`-Archimedean class
of the Hahn series.
 -/
hahnEmbedding_isOrderedAddMonoid : ∀ (M : Type u_1) [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M],
  ∃ f,
    Function.Injective ⇑f ∧
      ∀ (a : M), ArchimedeanClass.mk a = (FiniteArchimedeanClass.withTopOrderIso M) (ofLex (f a)).orderTop
-- Lean.DocString.Types
Lean.Doc.instOrdMathMode.ord : Lean.Doc.MathMode → Lean.Doc.MathMode → Ordering
-- Mathlib.Analysis.SpecificLimits.Normed
HasSummableGeomSeries.mk : ∀ {K : Type u_4} [inst : NormedRing K], (∀ (ξ : K), ‖ξ‖ < 1 → Summable fun n => ξ ^ n) → HasSummableGeomSeries K
-- Mathlib.RingTheory.MvPowerSeries.GaussNorm
/-- Given a multivariate power series `f` in, a function `v : R → ℝ` and a tuple `c` of real
numbers, the Gauss norm is defined as the supremum of the set of all values of
`v (coeff t f) * ∏ i : t.support, c i` for all `t : σ →₀ ℕ`.  -/
MvPowerSeries.gaussNorm : {R : Type u_1} → {σ : Type u_2} → (R → ℝ) → (σ → ℝ) → MvPowerSeries σ R → [Semiring R] → ℝ
-- Lean.Elab.Match
Lean.Elab.Term.GeneralizeResult.mk.sizeOf_spec : ∀ (discrs : Array Lean.Elab.Term.Discr) (toClear : Array Lean.FVarId) (matchType : Lean.Expr)
  (altViews : Array Lean.Elab.Term.TermMatchAltView) (refined : Bool),
  sizeOf { discrs := discrs, toClear := toClear, matchType := matchType, altViews := altViews, refined := refined } =
    1 + sizeOf discrs + sizeOf toClear + sizeOf matchType + sizeOf altViews + sizeOf refined
-- Mathlib.Tactic.ITauto
Mathlib.Tactic.ITauto.Proof.hyp.injEq : ∀ (n n_1 : Lean.Name), (Mathlib.Tactic.ITauto.Proof.hyp n = Mathlib.Tactic.ITauto.Proof.hyp n_1) = (n = n_1)
-- Mathlib.Analysis.Matrix.Normed
/-- This applies to the sup norm of L1 norm.  -/
Matrix.linftyOpNormSMulClass : ∀ {R : Type u_1} {m : Type u_3} {n : Type u_4} {α : Type u_5} [inst : Fintype m] [inst_1 : Fintype n]
  [inst_2 : SeminormedRing R] [inst_3 : SeminormedAddCommGroup α] [inst_4 : Module R α] [NormSMulClass R α],
  NormSMulClass R (Matrix m n α)
-- Mathlib.GroupTheory.OrderOfElement
orderOf_eq_zero_iff_eq_zero : ∀ {G₀ : Type u_6} [inst : GroupWithZero G₀] [Finite G₀] {a : G₀}, orderOf a = 0 ↔ a = 0
-- Mathlib.MeasureTheory.OuterMeasure.Induced
Option.elim'.eq_2 : ∀ {α : Type u_1} {β : Type u_2} (b : β) (f : α → β), Option.elim' b f none = b
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.cyclesMapIso_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (e : S₁ ≅ S₂) [inst_2 : S₁.HasLeftHomology] [inst_3 : S₂.HasLeftHomology],
  (CategoryTheory.ShortComplex.cyclesMapIso e).hom = CategoryTheory.ShortComplex.cyclesMap e.hom
-- Mathlib.RingTheory.Localization.Ideal
_private.Mathlib.RingTheory.Localization.Ideal.0.IsLocalization.map_ideal.eq_1 : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) (S : Type u_2) [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [inst_3 : IsLocalization M S] (I : Ideal R),
  IsLocalization.map_ideal✝ M S I = Submodule.localized' S M (Algebra.linearMap R S) I
-- Lean.Data.Lsp.Extra
Lean.Lsp.LeanPrepareModuleHierarchyParams.mk.injEq : ∀ (textDocument textDocument_1 : Lean.Lsp.TextDocumentIdentifier),
  ({ textDocument := textDocument } = { textDocument := textDocument_1 }) = (textDocument = textDocument_1)
-- Mathlib.LinearAlgebra.Prod
LinearMap.fst_surjective : ∀ {R : Type u} {M : Type v} {M₂ : Type w} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M₂]
  [inst_3 : Module R M] [inst_4 : Module R M₂], Function.Surjective ⇑(LinearMap.fst R M M₂)
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.IsPartition.eq_1 : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I), π.IsPartition = ∀ x ∈ I, ∃ J ∈ π, x ∈ J
-- Mathlib.Data.Finite.Defs
Set.not_infinite : ∀ {α : Type u} {s : Set α}, ¬s.Infinite ↔ s.Finite
-- Mathlib.Data.ENNReal.Operations
ENNReal.add_sub_add_eq_sub_right : ∀ {a b c : ENNReal}, autoParam (c ≠ ⊤) ENNReal.add_sub_add_eq_sub_right._auto_1 → a + c - (b + c) = a - b
-- Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
HurwitzKernelBounds.isBigO_atTop_F_int_one : ∀ (a : UnitAddCircle), ∃ p, 0 < p ∧ HurwitzKernelBounds.F_int 1 a =O[Filter.atTop] fun t => Real.exp (-p * t)
-- Mathlib.Topology.ContinuousMap.Compact
/-- If the pairwise products of continuous functions on a compact space are all zero, then the norm
of their sum is the maximum of their norms.  -/
ContinuousMap.nnnorm_sum_eq_sup : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : CompactSpace α] {R : Type u_4}
  [inst_2 : NonUnitalSeminormedRing R] [IsCancelMulZero R] {ι : Type u_5} {f : ι → C(α, R)} (s : Finset ι),
  Pairwise (Function.onFun (fun x1 x2 => x1 * x2 = 0) f) → ‖∑ i ∈ s, f i‖₊ = s.sup fun x => ‖f x‖₊
-- Mathlib.LinearAlgebra.Matrix.RowCol
Matrix.replicateCol_smul : ∀ {m : Type u_2} {R : Type u_5} {α : Type v} {ι : Type u_6} [inst : SMul R α] (x : R) (v : m → α),
  Matrix.replicateCol ι (x • v) = x • Matrix.replicateCol ι v
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Algebra.coe_inf : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (S T : Subalgebra R A),
  ↑(S ⊓ T) = ↑S ∩ ↑T
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.RightFraction.ofInv.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W : CategoryTheory.MorphismProperty C} {X Y : C}
  (s s_1 : Y ⟶ X) (e_s : s = s_1) (hs : W s),
  CategoryTheory.MorphismProperty.RightFraction.ofInv s hs = CategoryTheory.MorphismProperty.RightFraction.ofInv s_1 ⋯
-- Mathlib.Algebra.Order.Module.Defs
smul_one_strictMono : ∀ {α : Type u_1} (β : Type u_2) [inst : SMul α β] [inst_1 : Preorder α] [inst_2 : PartialOrder β] [inst_3 : Zero β]
  [inst_4 : One β] [ZeroLEOneClass β] [NeZero 1] [SMulPosStrictMono α β], StrictMono fun x => x • 1
-- Mathlib.Order.Hom.BoundedLattice
InfTopHomClass.toInfHomClass : ∀ {F : Type u_6} {α : Type u_7} {β : Type u_8} {inst : Min α} {inst_1 : Min β} {inst_2 : Top α} {inst_3 : Top β}
  {inst_4 : FunLike F α β} [self : InfTopHomClass F α β], InfHomClass F α β
-- Mathlib.Analysis.Calculus.Deriv.Mul
DifferentiableAt.finsetProd : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {ι : Type u_2} {𝔸' : Type u_3} [inst_1 : NormedCommRing 𝔸']
  [inst_2 : NormedAlgebra 𝕜 𝔸'] {u : Finset ι} {f : ι → 𝕜 → 𝔸'},
  (∀ i ∈ u, DifferentiableAt 𝕜 (f i) x) → DifferentiableAt 𝕜 (∏ i ∈ u, f i) x
-- Mathlib.Order.Filter.Ultrafilter.Defs
Ultrafilter.mem_or_compl_mem : ∀ {α : Type u} (f : Ultrafilter α) (s : Set α), s ∈ f ∨ sᶜ ∈ f
-- Mathlib.Data.EReal.Inv
EReal.div_pos : ∀ {a b : EReal}, 0 < a → 0 < b → b ≠ ⊤ → 0 < a / b
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.Measure.instIsLocallyFiniteMeasureForallVolumeOfSigmaFinite : ∀ {ι : Type u_1} [inst : Fintype ι] {X : ι → Type u_4} [inst_1 : (i : ι) → TopologicalSpace (X i)]
  [inst_2 : (i : ι) → MeasureTheory.MeasureSpace (X i)] [∀ (i : ι), MeasureTheory.SigmaFinite MeasureTheory.volume]
  [∀ (i : ι), MeasureTheory.IsLocallyFiniteMeasure MeasureTheory.volume],
  MeasureTheory.IsLocallyFiniteMeasure MeasureTheory.volume
-- Std.Data.DTreeMap.Internal.WF.Defs
Std.DTreeMap.Internal.Impl.WF.below.empty : ∀ {α : Type u} [inst : Ord α] {motive : {β : α → Type v} → (a : Std.DTreeMap.Internal.Impl α β) → a.WF → Prop}
  {x : α → Type v}, Std.DTreeMap.Internal.Impl.WF.below ⋯
-- Mathlib.Analysis.Calculus.FDeriv.Add
/-- **Alias** of the reverse direction of `differentiableWithinAt_add_const_iff`. -/
DifferentiableWithinAt.add_const : ∀ {𝕜 : 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} (c : F), DifferentiableWithinAt 𝕜 f s x → DifferentiableWithinAt 𝕜 (fun y => f y + c) s x
-- Mathlib.FieldTheory.Minpoly.ConjRootClass
ConjRootClass.mk_def : ∀ (K : Type u_1) {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] {x : L},
  ⟦x⟧ = ConjRootClass.mk K x
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
/-- **Alias** of `Function.Bijective.finsetSum`.

---

**Alias** of `Fintype.sum_bijective`.

---

`Fintype.sum_bijective` is a variant of `Finset.sum_bij` that accepts
`Function.Bijective`.

See `Function.Bijective.sum_comp` for a version without `h`.  -/
Function.Bijective.finset_sum : ∀ {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [inst : Fintype ι] [inst_1 : Fintype κ] [inst_2 : AddCommMonoid M]
  (e : ι → κ), Function.Bijective e → ∀ (f : ι → M) (g : κ → M), (∀ (x : ι), f x = g (e x)) → ∑ x, f x = ∑ x, g x
-- Mathlib.SetTheory.Lists
_private.Mathlib.SetTheory.Lists.0.Lists.mem.decidable.match_1.eq_2 : ∀ {α : Type u_1} (motive : Lists α → Lists' α true → Sort u_2) (a : Lists α) (b : Bool) (b_1 : Lists' α b)
  (l₂ : Lists' α true) (h_1 : (a : Lists α) → motive a Lists'.nil)
  (h_2 : (a : Lists α) → (b : Bool) → (b_2 : Lists' α b) → (l₂ : Lists' α true) → motive a (b_2.cons' l₂)),
  (match a, b_1.cons' l₂ with
    | a, Lists'.nil => h_1 a
    | a, b_2.cons' l₂ => h_2 a b b_2 l₂) =
    h_2 a b b_1 l₂
-- Mathlib.LinearAlgebra.FiniteDimensional.Basic
/-- If a submodule is contained in a finite-dimensional
submodule with the same or smaller dimension, they are equal.  -/
Submodule.eq_of_le_of_finrank_le : ∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  {S₁ S₂ : Submodule K V} [FiniteDimensional K ↥S₂], S₁ ≤ S₂ → Module.finrank K ↥S₂ ≤ Module.finrank K ↥S₁ → S₁ = S₂
-- Aesop.Tracing
Aesop.newNodeEmoji : String
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.XIsoOfEq_hom_comp_d : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (K : HomologicalComplex V c) {p₁ p₂ : ι}
  (h : p₁ = p₂) (p₃ : ι), CategoryTheory.CategoryStruct.comp (K.XIsoOfEq h).hom (K.d p₂ p₃) = K.d p₁ p₃
-- Mathlib.Analysis.Normed.Group.Pointwise
closedBall_add_singleton : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] (δ : ℝ) (x y : E),
  Metric.closedBall x δ + {y} = Metric.closedBall (x + y) δ
-- Mathlib.Analysis.Convex.Between
Sbtw.left_mem_image_Ioi : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Field R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R]
  [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P] {x y z : P},
  Sbtw R x y z → x ∈ ⇑(AffineMap.lineMap z y) '' Set.Ioi 1
-- Aesop.Search.Expansion
Aesop.SafeRuleResult : Type
-- Mathlib.RingTheory.FractionalIdeal.Operations
FractionalIdeal.coeIdeal_span_singleton : ∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  [inst_3 : IsLocalization S P] (x : R), ↑(Ideal.span {x}) = FractionalIdeal.spanSingleton S ((algebraMap R P) x)
-- Mathlib.Algebra.Order.Field.Basic
div_lt_div_right_of_neg : ∀ {α : Type u_2} [inst : Field α] [inst_1 : PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] {a b c : α},
  c < 0 → (a / c < b / c ↔ b < a)
-- Init.Data.Vector.Lemmas
Vector.swap_comm : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {i j : ℕ} (hi : i < n) (hj : j < n), xs.swap i j hi hj = xs.swap j i hj hi
-- Mathlib.LinearAlgebra.SpecialLinearGroup
LinearEquiv.smul_id_of_finrank_eq_one.eq_1 : ∀ {R : Type u_2} [inst : CommSemiring R] [inst_1 : StrongRankCondition R] {M : Type u_3} [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] [inst_4 : Module.Free R M] (d1 : Module.finrank R M = 1),
  LinearEquiv.smul_id_of_finrank_eq_one d1 =
    { toFun := fun c => c • LinearMap.id, map_add' := ⋯, map_smul' := ⋯, invFun := fun u => Exists.choose ⋯,
      left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.Algebra.Category.Semigrp.Basic
MagmaCat.coe_id : ∀ {X : MagmaCat}, ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) = id
-- Mathlib.Analysis.Calculus.Deriv.Comp
/-- The composition `l ∘ f` where `l : F → E` and `f : 𝕜 → F`, has a derivative equal to the
Fréchet derivative of `l` applied to the derivative of `f`.  -/
HasFDerivAt.comp_hasDerivAt_of_eq : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {E : Type w} [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace 𝕜 E] {f : 𝕜 → F}
  {f' : F} (x : 𝕜) {l : F → E} {l' : F →L[𝕜] E} {y : F},
  HasFDerivAt l l' y → HasDerivAt f f' x → y = f x → HasDerivAt (l ∘ f) (l' f') x
-- Mathlib.MeasureTheory.Measure.MutuallySingular
MeasureTheory.Measure.MutuallySingular.restrict_nullSet : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} (h : μ.MutuallySingular ν),
  μ.restrict h.nullSet = 0
-- Std.Tactic.BVDecide.LRAT.Internal.Assignment
Std.Tactic.BVDecide.LRAT.Internal.Assignment.removeNegAssignment.eq_3 : Std.Tactic.BVDecide.LRAT.Internal.Assignment.both.removeNegAssignment = Std.Tactic.BVDecide.LRAT.Internal.Assignment.pos
-- Mathlib.Algebra.Notation.Indicator
/-- See `Set.eqOn_mulIndicator'` for the version with `sᶜ`.  -/
Set.eqOn_mulIndicator : ∀ {α : Type u_1} {M : Type u_3} [inst : One M] {s : Set α} {f : α → M}, Set.EqOn (s.mulIndicator f) f s
-- Mathlib.Algebra.Vertex.HVertexOperator
HVertexOperator.coeff_inj_iff : ∀ {Γ : Type u_1} [inst : PartialOrder Γ] {R : Type u_2} {V : Type u_3} {W : Type u_4} [inst_1 : CommRing R]
  [inst_2 : AddCommGroup V] [inst_3 : Module R V] [inst_4 : AddCommGroup W] [inst_5 : Module R W]
  {a₁ a₂ : HVertexOperator Γ R V W}, a₁ = a₂ ↔ HVertexOperator.coeff a₁ = HVertexOperator.coeff a₂
-- Lean.Setup
Lean.Import.mk.injEq : ∀ (module : Lean.Name) (importAll isExported isMeta : Bool) (module_1 : Lean.Name)
  (importAll_1 isExported_1 isMeta_1 : Bool),
  ({ module := module, importAll := importAll, isExported := isExported, isMeta := isMeta } =
      { module := module_1, importAll := importAll_1, isExported := isExported_1, isMeta := isMeta_1 }) =
    (module = module_1 ∧ importAll = importAll_1 ∧ isExported = isExported_1 ∧ isMeta = isMeta_1)
-- Mathlib.CategoryTheory.Limits.ConeCategory
/-- If `F` has a colimit, then the colimit inclusions can be interpreted as costructured arrows
`F.obj - ⟶ colimit F`.  -/
CategoryTheory.Limits.colimit.toCostructuredArrow : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        (F : CategoryTheory.Functor J C) →
          [inst_2 : CategoryTheory.Limits.HasColimit F] →
            CategoryTheory.Functor J (CategoryTheory.CostructuredArrow F (CategoryTheory.Limits.colimit F))
-- Mathlib.NumberTheory.DirichletCharacter.Basic
/-- The conductor of `χ * ψ` divides the lcm of the conductors of `χ` and `ψ`.  -/
DirichletCharacter.conductor_mul_dvd_lcm_conductor : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] {n : ℕ} (χ ψ : DirichletCharacter R n),
  (χ * ψ).conductor ∣ χ.conductor.lcm ψ.conductor
-- Mathlib.CategoryTheory.Limits.Comma
CategoryTheory.Comma.coconeOfPreserves_ι_app_left : ∀ {J : Type w} [inst : CategoryTheory.Category.{w', w} J] {A : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} A]
  {B : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃}
  [inst_3 : CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T}
  (F : CategoryTheory.Functor J (CategoryTheory.Comma L R))
  [inst_4 : CategoryTheory.Limits.PreservesColimit (F.comp (CategoryTheory.Comma.fst L R)) L]
  {c₁ : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.Comma.fst L R))} (t₁ : CategoryTheory.Limits.IsColimit c₁)
  (c₂ : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.Comma.snd L R))) (j : J),
  ((CategoryTheory.Comma.coconeOfPreserves F t₁ c₂).ι.app j).left = c₁.ι.app j
-- Lean.Elab.Tactic.Split
_private.Lean.Elab.Tactic.Split.0.Lean.Elab.Tactic.evalSplit.mkCasesHint : Lean.Expr → Lean.MessageData
-- Mathlib.Geometry.Convex.Cone.Dual
PointedCone.dual_zero : ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] {N : Type u_3} [inst_5 : AddCommMonoid N] [inst_6 : Module R N]
  {p : M →ₗ[R] N →ₗ[R] R}, PointedCone.dual p 0 = ⊤
-- Mathlib.Order.Part
Antitone.partMap : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Preorder α] {f : β → γ} {g : α → Part β},
  Antitone g → Antitone fun x => Part.map f (g x)
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
CategoryTheory.Subobject.Classifier.ofIso_χ₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (𝒞 : CategoryTheory.Subobject.Classifier C) {Ω₀ Ω : C}
  (eΩ : 𝒞.Ω ≅ Ω) (eΩ₀ : 𝒞.Ω₀ ≅ Ω₀) (from' : (C_1 : C) → C_1 ⟶ Ω₀) (t : Ω₀ ⟶ Ω)
  (ht :
    autoParam (t = CategoryTheory.CategoryStruct.comp eΩ₀.inv (CategoryTheory.CategoryStruct.comp 𝒞.truth eΩ.hom))
      CategoryTheory.Subobject.Classifier.ofIso._auto_1)
  (C_1 : C), (𝒞.ofIso eΩ eΩ₀ from' t ht).χ₀ C_1 = from' C_1
-- Mathlib.Order.Filter.AtTopBot.Basic
Filter.map_add_atTop_eq_nat : ∀ (k : ℕ), Filter.map (fun a => a + k) Filter.atTop = Filter.atTop
-- Mathlib.Order.Bounds.Basic
IsLUB.inter_Ici_of_mem : ∀ {γ : Type u_3} [inst : LinearOrder γ] {s : Set γ} {a b : γ}, IsLUB s a → b ∈ s → IsLUB (s ∩ Set.Ici b) a
-- Std.Data.ExtDTreeMap.Basic
/-- Tries to retrieve the largest key in the tree map, panicking if the map is empty.
 -/
Std.ExtDTreeMap.maxKey! : {α : Type u} →
  {β : α → Type v} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → [Inhabited α] → Std.ExtDTreeMap α β cmp → α
-- Mathlib.Data.Setoid.Basic
/-- A special case of the equivalence closure of an equivalence relation r equaling r.  -/
Setoid.mapOfSurjective_eq_map : ∀ {α : Type u_1} {β : Type u_2} {r : Setoid α} {f : α → β} (h : Setoid.ker f ≤ r) (hf : Function.Surjective f),
  r.map f = r.mapOfSurjective f h hf
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.mk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X : C} →
      (arrows : CategoryTheory.Presieve X) →
        (∀ {Y Z : C} {f : Y ⟶ X}, arrows f → ∀ (g : Z ⟶ Y), arrows (CategoryTheory.CategoryStruct.comp g f)) →
          CategoryTheory.Sieve X
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.liftPred_coe : ∀ {α : Type u_1} {β : Type u_2} {l : Filter α} {p : β → Prop} {f : α → β},
  Filter.Germ.LiftPred p ↑f ↔ ∀ᶠ (x : α) in l, p (f x)