mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Normed.Group.Defs
SeminormedGroup.ofMulDist'.eq_1 : ∀ {E : Type u_5} [inst : Norm E] [inst_1 : Group E] [inst_2 : PseudoMetricSpace E] (h₁ : ∀ (x : E), ‖x‖ = dist 1 x)
  (h₂ : ∀ (x y z : E), dist (z * x) (z * y) ≤ dist x y),
  SeminormedGroup.ofMulDist' h₁ h₂ = { toNorm := inst, toGroup := inst_1, toPseudoMetricSpace := inst_2, dist_eq := ⋯ }
-- Mathlib.Algebra.MonoidAlgebra.Lift
/-- A non-commutative version of `MonoidAlgebra.lift`: given an additive homomorphism `f : k →+ R`
and a homomorphism `g : G → R`, returns the additive homomorphism from
`k[G]` such that `liftNC f g (single a b) = f b * g a`. If `f` is a ring homomorphism
and the range of either `f` or `g` is in center of `R`, then the result is a ring homomorphism.  If
`R` is a `k`-algebra and `f = algebraMap k R`, then the result is an algebra homomorphism called
`MonoidAlgebra.lift`.  -/
MonoidAlgebra.liftNC : {k : Type u₁} →
  {G : Type u₂} →
    {R : Type u_2} →
      [inst : Semiring k] → [inst_1 : NonUnitalNonAssocSemiring R] → (k →+ R) → (G → R) → MonoidAlgebra k G →+ R
-- Mathlib.Geometry.Manifold.LocalInvariantProperties
StructureGroupoid.HasGroupoid.comp : ∀ {H₁ : Type u_6} [inst : TopologicalSpace H₁] {H₂ : Type u_7} [inst_1 : TopologicalSpace H₂] {H₃ : Type u_8}
  [inst_2 : TopologicalSpace H₃] [inst_3 : ChartedSpace H₁ H₂] [inst_4 : ChartedSpace H₂ H₃] {G₁ : StructureGroupoid H₁}
  [HasGroupoid H₂ G₁] [ClosedUnderRestriction G₁] (G₂ : StructureGroupoid H₂) [HasGroupoid H₃ G₂],
  (∀ e ∈ G₂, ChartedSpace.LiftPropOn G₁.IsLocalStructomorphWithinAt (↑e) e.source) → HasGroupoid H₃ G₁
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValue?_replaceEntry_of_false : ∀ {α : Type u} {β : Type v} [inst : BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {k a : α} {v : β},
  (k == a) = false →
    Std.Internal.List.getValue? a (Std.Internal.List.replaceEntry k v l) = Std.Internal.List.getValue? a l
-- Mathlib.Data.Nat.Prime.Basic
Nat.eq_one_iff_not_exists_prime_dvd : ∀ {n : ℕ}, n = 1 ↔ ∀ (p : ℕ), Nat.Prime p → ¬p ∣ n
-- Lean.Data.JsonRpc
Lean.JsonRpc.MessageDirection.clientToServer : Lean.JsonRpc.MessageDirection
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
IsCyclotomicExtension.Rat.span_zeta_sub_one_ne_bot : ∀ (p k : ℕ) [hp : Fact (Nat.Prime p)] {K : Type u_1} [inst : Field K] [inst_1 : NumberField K]
  [hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K] {ζ : K} (hζ : IsPrimitiveRoot ζ (p ^ (k + 1))),
  Ideal.span {hζ.toInteger - 1} ≠ ⊥
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.contains_modify : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {k k' : α} {f : β k → β k}, (t.modify k f).contains k' = t.contains k'
-- Mathlib.Topology.Sober
genericPoints.finite : ∀ {α : Type u_1} [inst : TopologicalSpace α] [T0Space α], (irreducibleComponents α).Finite → (genericPoints α).Finite
-- Mathlib.SetTheory.Cardinal.Regular
Cardinal.IsSingular.isSuccLimit : ∀ {c : Cardinal.{u_1}}, c.IsSingular → Order.IsSuccLimit c
-- Init.Data.SInt.Lemmas
Int16.ofBitVec_lt_iff_slt : ∀ (a b : BitVec 16), Int16.ofBitVec a < Int16.ofBitVec b ↔ a.slt b = true
-- Mathlib.LinearAlgebra.Alternating.Basic
AlternatingMap.instZero : {R : Type u_1} →
  [inst : Semiring R] →
    {M : Type u_2} →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] →
          {N : Type u_3} → [inst_3 : AddCommMonoid N] → [inst_4 : Module R N] → {ι : Type u_7} → Zero (M [⋀^ι]→ₗ[R] N)
-- Mathlib.Topology.Algebra.Group.Pointwise
IsTopologicalAddGroup.regularSpace : ∀ (G : Type w) [inst : TopologicalSpace G] [inst_1 : AddGroup G] [IsTopologicalAddGroup G], RegularSpace G
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
MeasurableSet.subtype_image : ∀ {α : Type u_1} {m : MeasurableSpace α} {s : Set α} {t : Set ↑s},
  MeasurableSet s → MeasurableSet t → MeasurableSet (Subtype.val '' t)
-- Mathlib.CategoryTheory.Limits.Final
CategoryTheory.Functor.Final.preservesColimit_of_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [F.Final] {E : Type u₃} [inst_3 : CategoryTheory.Category.{v₃, u₃} E]
  {G : CategoryTheory.Functor D E} {B : Type u₄} [inst_4 : CategoryTheory.Category.{v₄, u₄} B]
  {H : CategoryTheory.Functor E B} [CategoryTheory.Limits.PreservesColimit (F.comp G) H],
  CategoryTheory.Limits.PreservesColimit G H
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.LetRecToLift.type : Lean.Elab.Term.LetRecToLift → Lean.Expr
-- Mathlib.NumberTheory.LSeries.Linearity
LSeriesSummable.add : ∀ {f g : ℕ → ℂ} {s : ℂ}, LSeriesSummable f s → LSeriesSummable g s → LSeriesSummable (f + g) s
-- Mathlib.Algebra.Colimit.Module
Module.DirectLimit.induction_on : ∀ {R : Type u_1} [inst : Semiring R] {ι : Type u_2} [inst_1 : Preorder ι] {G : ι → Type u_3}
  [inst_2 : (i : ι) → AddCommMonoid (G i)] [inst_3 : (i : ι) → Module R (G i)] {f : (i j : ι) → i ≤ j → G i →ₗ[R] G j}
  [inst_4 : DecidableEq ι] [Nonempty ι] [IsDirectedOrder ι] {C : Module.DirectLimit G f → Prop}
  (z : Module.DirectLimit G f), (∀ (i : ι) (x : G i), C ((Module.DirectLimit.of R ι G f i) x)) → C z
-- Lean.Parser.Basic
/-- Parses an hexadecimal numeral without the `0x` prefix. It is not a literal.  -/
Lean.Parser.hexnumFn : Lean.Parser.ParserFn
-- Mathlib.Algebra.Field.Defs
NNRat.cast_def : ∀ {K : Type u_1} [inst : DivisionSemiring K] (q : ℚ≥0), ↑q = ↑q.num / ↑q.den
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.instIsCutFlipOrderingSwap : ∀ {α : Type u_1} (cmp : α → α → Ordering) (cut : α → Ordering) [RBTree.RBNode.IsCut cmp cut],
  RBTree.RBNode.IsCut (flip cmp) fun x => (cut x).swap
-- Init.MetaTypes
/-- In applications, do reductions of implicit arguments. Default: `false`.  -/
Lean.Meta.Command.ReduceConfig.implicits : Lean.Meta.Command.ReduceConfig → Bool
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.instIsPrimeSupp : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R], (ValuativeRel.supp R).IsPrime
-- Mathlib.Combinatorics.SimpleGraph.Paths
/-- **Alias** of `SimpleGraph.Walk.edges_bypass_subset_edges`. -/
SimpleGraph.Walk.edges_bypass_subset : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} [inst : DecidableEq V] (p : G.Walk u v), p.bypass.edges ⊆ p.edges
-- Mathlib.Algebra.GroupWithZero.NonZeroDivisors
/-- If an element maps to a non-zero-divisor via injective homomorphism,
then it is a non-zero-divisor.  -/
mem_nonZeroDivisors_of_injective : ∀ {F : Type u_1} {M₀ : Type u_2} {M₀' : Type u_3} [inst : MonoidWithZero M₀] [inst_1 : MonoidWithZero M₀'] {x : M₀}
  [inst_2 : FunLike F M₀ M₀'] [MonoidWithZeroHomClass F M₀ M₀'] {f : F},
  Function.Injective ⇑f → f x ∈ nonZeroDivisors M₀' → x ∈ nonZeroDivisors M₀
-- Mathlib.Algebra.Homology.ShortComplex.ShortExact
CategoryTheory.ShortComplex.ShortExact.mk' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C}, S.Exact → CategoryTheory.Mono S.f → CategoryTheory.Epi S.g → S.ShortExact
-- Lean.Elab.InfoTree.Types
Lean.Elab.TacticInfo.toElabInfo : Lean.Elab.TacticInfo → Lean.Elab.ElabInfo
-- Mathlib.LinearAlgebra.Dimension.Basic
/-- If `S / R` and `S' / R'` are algebras, `i : R ≃+* R'` and `j : S ≃+* S'` are
ring isomorphisms, such that `R → R' → S'` and `R → S → S'` commute,
then the rank of `S / R` is equal to the rank of `S' / R'`.  -/
Algebra.lift_rank_eq_of_equiv_equiv : ∀ {R : Type w} {S : Type v} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] {R' : Type w'}
  {S' : Type v'} [inst_3 : CommSemiring R'] [inst_4 : Semiring S'] [inst_5 : Algebra R' S'] (i : R ≃+* R')
  (j : S ≃+* S'),
  (algebraMap R' S').comp i.toRingHom = j.toRingHom.comp (algebraMap R S) →
    Cardinal.lift.{v', v} (Module.rank R S) = Cardinal.lift.{v, v'} (Module.rank R' S')
-- Mathlib.Algebra.Notation.Pi.Basic
Pi.curry_single : ∀ {ι : Type u_1} {ι' : Type u_2} [inst : DecidableEq ι] {M : Type u_9} [inst_1 : Zero M] [inst_2 : DecidableEq ι']
  (i : ι × ι') (b : M), Function.curry (Pi.single i b) = Pi.single i.1 (Pi.single i.2 b)
-- Mathlib.Algebra.Homology.HomotopyCategory.Shift
HomotopyCategory.instAdditiveIntUpShiftFunctor : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] (n : ℤ),
  (CategoryTheory.shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) n).Additive
-- Std.Sync.Channel
_private.Std.Sync.Channel.0.Std.CloseableChannel.Bounded.mk.injEq : ∀ {α : Type} (state state_1 : Std.Mutex (Std.CloseableChannel.Bounded.State✝ α)),
  ({ state := state } = { state := state_1 }) = (state = state_1)
-- Mathlib.FieldTheory.PolynomialGaloisGroup
Polynomial.Gal.restrictProd.eq_1 : ∀ {F : Type u_1} [inst : Field F] (p q : Polynomial F),
  Polynomial.Gal.restrictProd p q = (Polynomial.Gal.restrictDvd ⋯).prod (Polynomial.Gal.restrictDvd ⋯)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.isEmpty_of_isEmpty_insertManyIfNewUnit : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α Unit} {ρ : Type w} [inst_2 : ForIn Id ρ α]
  [EquivBEq α] [LawfulHashable α], m.WF → ∀ {l : ρ}, (m.insertManyIfNewUnit l).isEmpty = true → m.isEmpty = true
-- Mathlib.Order.Monotone.Monovary
Subsingleton.antivary : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] [Subsingleton ι] (f : ι → α)
  (g : ι → β), Antivary f g
-- Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms
CategoryTheory.ObjectProperty.le_isoClosure : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C), P ≤ P.isoClosure
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.mk : {K : Type u} →
  [inst : Field K] →
    (toSubring : Subring K) → (∀ (x : K), x ∈ toSubring.carrier ∨ x⁻¹ ∈ toSubring.carrier) → ValuationSubring K
-- Mathlib.NumberTheory.Padics.PadicIntegers
PadicInt.instIsLocalRing : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)], IsLocalRing ℤ_[p]
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range
range_cfc : ∀ (𝕜 : Type u_1) {A : Type u_2} {p : A → Prop} [inst : RCLike 𝕜] [inst_1 : Ring A] [inst_2 : StarRing A]
  [inst_3 : Algebra 𝕜 A] [inst_4 : TopologicalSpace A] [inst_5 : StarModule 𝕜 A]
  [inst_6 : ClosedEmbeddingContinuousFunctionalCalculus 𝕜 A p] [inst_7 : IsTopologicalRing A]
  [inst_8 : ContinuousStar A] {a : A}, p a → (Set.range fun x => cfc x a) = ↑(StarAlgebra.elemental 𝕜 a)
-- Aesop.Rule
Aesop.LocalNormSimpRule.instHashable : Hashable Aesop.LocalNormSimpRule
-- Mathlib.Data.Multiset.Lattice
Multiset.le_inf : ∀ {α : Type u_1} [inst : SemilatticeInf α] [inst_1 : OrderTop α] {s : Multiset α} {a : α}, a ≤ s.inf ↔ ∀ b ∈ s, a ≤ b
-- Init.Data.List.Basic
List.Mem.below.tail : ∀ {α : Type u} {a : α} {motive : (a_1 : List α) → List.Mem a a_1 → Prop} (b : α) {as : List α} (a_1 : List.Mem a as),
  List.Mem.below a_1 → motive as a_1 → List.Mem.below ⋯
-- Mathlib.Data.WSeq.Relation
Stream'.WSeq.bind_congr : ∀ {α : Type u} {β : Type v} {s1 s2 : Stream'.WSeq α} {f1 f2 : α → Stream'.WSeq β},
  s1 ~ʷ s2 → (∀ (a : α), f1 a ~ʷ f2 a) → s1.bind f1 ~ʷ s2.bind f2
-- Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
/-- Pushforward of a summation filter along an embedding.

(We define this only for embeddings, rather than arbitrary maps, since this is the only case needed
for the intended applications, and this avoids requiring a `DecidableEq` instance on `γ`.)  -/
SummationFilter.map : {β : Type u_2} → {γ : Type u_3} → SummationFilter β → (β ↪ γ) → SummationFilter γ
-- Init.Data.List.Attach
List.map_pmap : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {p : α → Prop} {g : β → γ} {f : (a : α) → p a → β} {l : List α}
  (H : ∀ a ∈ l, p a), List.map g (List.pmap f l H) = List.pmap (fun a h => g (f a h)) l H
-- Mathlib.Algebra.Order.Group.DenselyOrdered
le_of_forall_lt_one_mul_le : ∀ {α : Type u_1} [inst : Group α] [inst_1 : LinearOrder α] [MulLeftMono α] [DenselyOrdered α] {a b : α},
  (∀ ε < 1, a * ε ≤ b) → a ≤ b
-- Mathlib.Probability.Distributions.Gaussian.Real
ProbabilityTheory.gaussianPDFReal_inv_mul : ∀ {μ : ℝ} {v : NNReal} {c : ℝ},
  c ≠ 0 →
    ∀ (x : ℝ),
      ProbabilityTheory.gaussianPDFReal μ v (c⁻¹ * x) =
        |c| * ProbabilityTheory.gaussianPDFReal (c * μ) (NNReal.mk (c ^ 2) ⋯ * v) x
-- Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
/-- A simple sufficient condition for bounding `levyProkhorovDist` between probability measures
from above. The condition involves only one of two natural bounds, the other bound is for free.  -/
MeasureTheory.levyProkhorovDist_le_of_forall_le : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : PseudoEMetricSpace Ω] [OpensMeasurableSpace Ω]
  (μ ν : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] {δ : ℝ},
  0 ≤ δ →
    (∀ (ε : ℝ) (B : Set Ω), δ < ε → MeasurableSet B → μ B ≤ ν (Metric.thickening ε B) + ENNReal.ofReal ε) →
      MeasureTheory.levyProkhorovDist μ ν ≤ δ
-- Mathlib.CategoryTheory.Filtered.Basic
CategoryTheory.isFilteredOrEmpty_of_directed_le : ∀ (α : Type u) [inst : Preorder α] [IsDirectedOrder α], CategoryTheory.IsFilteredOrEmpty α
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.PreInstance.proof : Lean.Meta.Grind.PreInstance → Lean.Expr
-- Mathlib.Tactic.Algebraize
_private.Mathlib.Tactic.Algebraize.0.Mathlib.Tactic.Algebraize.instEvalExprConfig : Lean.Elab.ConfigEval.EvalExpr Mathlib.Tactic.Algebraize.Config
-- Lean.Elab.Match
Lean.Elab.Term.ToDepElimPattern.State.mk : Array Lean.Expr → Lean.Elab.Term.ToDepElimPattern.State
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.size_add_size_eq_size_union_add_size_inter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp],
  t₁.size + t₂.size = (t₁ ∪ t₂).size + (t₁ ∩ t₂).size
-- Mathlib.Analysis.PSeries
/-- Test for convergence of the `p`-series: the real-valued series `∑' n : ℕ, 1 / n ^ p` converges
if and only if `1 < p`.  -/
Real.summable_one_div_nat_pow : ∀ {p : ℕ}, (Summable fun n => 1 / ↑n ^ p) ↔ 1 < p
-- Lean.Setup
Lean.ModuleArtifacts.bc? : Lean.ModuleArtifacts → Option System.FilePath
-- Mathlib.CategoryTheory.MorphismProperty.Concrete
CategoryTheory.MorphismProperty.instIsMultiplicativeBijective : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type u_2}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC],
  (CategoryTheory.MorphismProperty.bijective C).IsMultiplicative
-- Mathlib.Analysis.Convex.Topology
/-- **Alias** of `Convex.sdiff_singleton_eventually_mem_nhds`. -/
Convex.diff_singleton_eventually_mem_nhds : ∀ {𝕜 : Type u_4} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [inst_3 : TopologicalSpace 𝕜]
  [OrderTopology 𝕜] {s : Set 𝕜}, Convex 𝕜 s → ∀ (a : 𝕜), ∀ᶠ (x : 𝕜) in nhdsWithin a (s \ {a}), s \ {a} ∈ nhds x
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
MeasureTheory.setLIntegral_nnnorm_condExpIndSMul_le : ∀ {α : Type u_1} {G : Type u_5} [inst : NormedAddCommGroup G] {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {s : Set α} [inst_1 : NormedSpace ℝ G] (hm : m ≤ m0) (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) (x : G) {t : Set α},
  MeasurableSet t → μ t ≠ ⊤ → ∫⁻ (a : α) in t, ↑‖↑↑(MeasureTheory.condExpIndSMul hm hs hμs x) a‖₊ ∂μ ≤ μ (s ∩ t) * ↑‖x‖₊
-- Mathlib.Order.SupIndep
/-- Supremum independence of finite sets. We avoid the "obvious" definition using `s.erase i`
because `erase` would require decidable equality on `ι`.  -/
Finset.SupIndep : {α : Type u_1} → {ι : Type u_3} → [inst : Lattice α] → [OrderBot α] → Finset ι → (ι → α) → Prop
-- Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers
/-- The pullback of two monomorphisms exists.  -/
CategoryTheory.NormalMonoCategory.pullback_of_mono : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasKernels C]
  [CategoryTheory.IsNormalMonoCategory C] {X Y Z : C} (a : X ⟶ Z) (b : Y ⟶ Z) [CategoryTheory.Mono a]
  [CategoryTheory.Mono b], CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.cospan a b)
-- Lean.Meta.Constructions.NoConfusion
_private.Lean.Meta.Constructions.NoConfusion.0.Lean.mkNoConfusionType : Lean.Name → Lean.MetaM Unit
-- Mathlib.Logic.Relation
Quot.eqvGen_sound : ∀ {α : Type u_1} {r : α → α → Prop} {a b : α}, Relation.EqvGen r a b → Quot.mk r a = Quot.mk r b
-- Plausible.Testable
Plausible.TestResult.failure.injEq : ∀ {p : Prop} (a : ¬p) (a_1 : List String) (a_2 : ℕ) (a_3 : ¬p) (a_4 : List String) (a_5 : ℕ),
  (Plausible.TestResult.failure a a_1 a_2 = Plausible.TestResult.failure a_3 a_4 a_5) = (a_1 = a_4 ∧ a_2 = a_5)
-- Mathlib.Topology.MetricSpace.GromovHausdorff
_private.Mathlib.Topology.MetricSpace.GromovHausdorff.0.termℓ_infty_ℝ : Lean.ParserDescr
-- Mathlib.Algebra.MonoidAlgebra.PointwiseSMul
/-- A convolution-type scalar multiplication of the monoid algebra on the set of formal
functions.  -/
MonoidAlgebra.instSMulForallOfIsLeftCancelSMulOfSMulWithZero : {G : Type u_1} →
  {P : Type u_2} →
    {R : Type u_3} →
      {V : Type u_4} →
        [inst : SMul G P] →
          [IsLeftCancelSMul G P] →
            [inst : Semiring R] → [inst_1 : AddCommMonoid V] → [SMulWithZero R V] → SMul (MonoidAlgebra R G) (P → V)
-- Mathlib.Topology.Algebra.Group.Basic
topologicalAddGroup_of_discreteTopology : ∀ {H : Type x} [inst : TopologicalSpace H] [inst_1 : AddGroup H] [DiscreteTopology H], IsTopologicalAddGroup H
-- Mathlib.Algebra.Lie.Basic
LieModuleHom.hasZSMul : {R : Type u} →
  {L : Type v} →
    {M : Type w} →
      {N : Type w₁} →
        [inst : CommRing R] →
          [inst_1 : LieRing L] →
            [inst_2 : AddCommGroup M] →
              [inst_3 : AddCommGroup N] →
                [inst_4 : Module R M] →
                  [inst_5 : Module R N] →
                    [inst_6 : LieRingModule L M] → [inst_7 : LieRingModule L N] → SMul ℤ (M →ₗ⁅R,L⁆ N)
-- Mathlib.Data.Set.Finite.Range
Set.Finite.dependent_image : ∀ {α : Type u} {β : Type v} {s : Set α},
  s.Finite → ∀ (F : (i : α) → i ∈ s → β), {y | ∃ x, ∃ (hx : x ∈ s), F x hx = y}.Finite
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology
CochainComplex.HomComplex.instAddCommGroupCohomologyClass : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      (K L : CochainComplex C ℤ) → (n : ℤ) → AddCommGroup (CochainComplex.HomComplex.CohomologyClass K L n)
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.C_inj : ∀ {σ : Type u_2} (R : Type u_3) [inst : CommSemiring R] (r s : R), MvPolynomial.C r = MvPolynomial.C s ↔ r = s
-- Lean.Elab.Tactic.Try
/-- `simple` tactics  -/
_private.Lean.Elab.Tactic.Try.0.Lean.Elab.Tactic.Try.mkSimpleTacStx : Lean.CoreM (Lean.TSyntax `tactic)
-- Mathlib.MeasureTheory.Measure.Tight
/-- A set of measures on a product space is tight if both marginals are tight.  -/
MeasureTheory.IsTightMeasureSet.prodMk : ∀ {𝓧 : Type u_1} {𝓨 : Type u_2} {m𝓧 : MeasurableSpace 𝓧} [inst : TopologicalSpace 𝓧] {m𝓨 : MeasurableSpace 𝓨}
  [inst_1 : TopologicalSpace 𝓨] {μ : Set (MeasureTheory.Measure (𝓧 × 𝓨))},
  MeasureTheory.IsTightMeasureSet (MeasureTheory.Measure.fst '' μ) →
    MeasureTheory.IsTightMeasureSet (MeasureTheory.Measure.snd '' μ) → MeasureTheory.IsTightMeasureSet μ
-- Std.Data.HashMap.Lemmas
Std.HashMap.getElem_eq_getD : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {a : α}
  {fallback : β} {h' : a ∈ m}, m[a] = m.getD a fallback
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.maxKey_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  {h' : t₁.isEmpty = false} (h : t₁.Equiv t₂), t₁.maxKey h' = t₂.maxKey ⋯
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.subsingleton_iff : ∀ {V : Type u}, Subsingleton (SimpleGraph V) ↔ Subsingleton V
-- Init.Data.Int.DivMod.Lemmas
Int.neg_emod_eq_sub_emod : ∀ {a b : ℤ}, -a % b = (b - a) % b
-- Mathlib.Algebra.Star.Unitary
Unitary.coe_zpow : ∀ {R : Type u_1} [inst : GroupWithZero R] [inst_1 : StarMul R] (U : ↥(unitary R)) (z : ℤ), ↑(U ^ z) = ↑U ^ z
-- Mathlib.RingTheory.PowerSeries.Derivative
PowerSeries.derivative_C : ∀ {R : Type u_1} [inst : CommSemiring R] {r : R}, (PowerSeries.derivative R) (PowerSeries.C r) = 0
-- Init.Data.UInt.Lemmas
UInt16.ofNat_uInt64ToNat : ∀ (n : UInt64), UInt16.ofNat n.toNat = n.toUInt16
-- Std.Sat.AIG.Basic
/-- A collection of 3 of `Ref`s, useful for `LawfulOperator`s that act on three `Ref`s at a time,
in particular multiplexer style functions.
 -/
Std.Sat.AIG.TernaryInput : {α : Type} → [inst : Hashable α] → [inst_1 : DecidableEq α] → Std.Sat.AIG α → Type
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable
measurable_of_tendsto_metrizable_ae : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace β]
  [TopologicalSpace.PseudoMetrizableSpace β] [inst_3 : MeasurableSpace β] [BorelSpace β] {μ : MeasureTheory.Measure α}
  [μ.IsComplete] {f : ℕ → α → β} {g : α → β},
  (∀ (n : ℕ), Measurable (f n)) →
    (∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun n => f n x) Filter.atTop (nhds (g x))) → Measurable g
-- Mathlib.MeasureTheory.Measure.AEDisjoint
/-- **Alias** of `MeasureTheory.AEDisjoint.measure_sdiff_right`. -/
MeasureTheory.AEDisjoint.measure_diff_right : ∀ {α : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
  MeasureTheory.AEDisjoint μ s t → μ (t \ s) = μ t
-- Mathlib.Algebra.Order.Interval.Set.Instances
Set.Ioo.one_minus_pos : ∀ {β : Type u_2} [inst : Ring β] [inst_1 : PartialOrder β] [IsOrderedRing β] (x : ↑(Set.Ioo 0 1)), 0 < 1 - ↑x
-- Mathlib.LinearAlgebra.Complex.Module
realPart_surjective : ∀ {A : Type u_1} [inst : AddCommGroup A] [inst_1 : Module ℂ A] [inst_2 : StarAddMonoid A] [inst_3 : StarModule ℂ A],
  Function.Surjective ⇑realPart
-- Mathlib.Topology.Homotopy.HomotopyGroup
GenLoop.genLoopGenLoopEquiv_symm_apply_coe : ∀ {N : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {M : Type u_3} (x : X) (q : ↑(GenLoop (M ⊕ N) X x)),
  ↑((GenLoop.genLoopGenLoopEquiv x).symm q) = GenLoop.currySum x q
-- Mathlib.NumberTheory.LucasLehmer
/-- The recurrence `s (i+1) = (s i)^2 - 2` in `ℤ`.  -/
LucasLehmer.s : ℕ → ℤ
-- Lean.Message
Lean.BaseMessage.caption : {α : Type u} → Lean.BaseMessage α → String
-- Mathlib.Algebra.Homology.DerivedCategory.ShortExact
DerivedCategory.triangleOfSES.map_hom₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] {S₁ S₂ : CategoryTheory.ShortComplex (CochainComplex C ℤ)} (h₁ : S₁.ShortExact)
  (h₂ : S₂.ShortExact) (f : S₁ ⟶ S₂), (DerivedCategory.triangleOfSES.map h₁ h₂ f).hom₂ = DerivedCategory.Q.map f.τ₂
-- Lean.Exception
Lean.Exception.error.inj : ∀ {ref : Lean.Syntax} {msg : Lean.MessageData} {ref_1 : Lean.Syntax} {msg_1 : Lean.MessageData},
  Lean.Exception.error ref msg = Lean.Exception.error ref_1 msg_1 → ref = ref_1 ∧ msg = msg_1
-- Mathlib.CategoryTheory.Sites.IsSheafFor
CategoryTheory.Presieve.IsSheafFor.valid_glue : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X Y : C}
  {R : CategoryTheory.Presieve X} (t : CategoryTheory.Presieve.IsSheafFor P R)
  {x : CategoryTheory.Presieve.FamilyOfElements P R} (hx : x.Compatible) (f : Y ⟶ X) (Hf : R f),
  (CategoryTheory.ConcreteCategory.hom (P.map f.op)) (t.amalgamate x hx) = x f Hf
-- Mathlib.Algebra.Ring.Ext
NonUnitalSemiring.toNonUnitalNonAssocSemiring_injective : ∀ {R : Type u}, Function.Injective (@NonUnitalSemiring.toNonUnitalNonAssocSemiring R)
-- Mathlib.Algebra.Group.Invertible.Defs
invOf_mul_cancel_left' : ∀ {α : Type u} [inst : Monoid α] (a b : α) {x : Invertible a}, ⅟a * (a * b) = b
-- Init.Data.Int.DivMod.Bootstrap
Int.add_mul_ediv_right : ∀ (a b : ℤ) {c : ℤ}, c ≠ 0 → (a + b * c) / c = a / c + b
-- Lean.Data.Lsp.TextSync
Lean.Lsp.SaveOptions.mk.inj : ∀ {includeText includeText_1 : Bool},
  { includeText := includeText } = { includeText := includeText_1 } → includeText = includeText_1
-- Lean.Meta.CongrTheorems
_private.Lean.Meta.CongrTheorems.0.Lean.Meta.mkCongrSimpCore?.mkProof.go : Array Lean.Meta.CongrArgKind → ℕ → Lean.Expr → Lean.MetaM Lean.Expr