mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.Algebra.Monoid
instOneContMDiffMonoidMorphism.eq_1 : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {H : Type u_2} [inst_1 : TopologicalSpace H]
  {E : Type u_3} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4}
  [inst_4 : Monoid G] [inst_5 : TopologicalSpace G] [inst_6 : ChartedSpace H G] {H' : Type u_5}
  [inst_7 : TopologicalSpace H'] {E' : Type u_6} [inst_8 : NormedAddCommGroup E'] [inst_9 : NormedSpace 𝕜 E']
  {I' : ModelWithCorners 𝕜 E' H'} {G' : Type u_7} [inst_10 : Monoid G'] [inst_11 : TopologicalSpace G']
  [inst_12 : ChartedSpace H' G'],
  instOneContMDiffMonoidMorphism =
    {
      one :=
        let __MonoidHom := 1;
        { toMonoidHom := __MonoidHom, contMDiff_toFun := ⋯ } }
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVExpr.eval_replicate : ∀ {assign : Std.Tactic.BVDecide.BVExpr.Assignment} {n a : ℕ} {expr : Std.Tactic.BVDecide.BVExpr a} {h : a * n = a * n},
  Std.Tactic.BVDecide.BVExpr.eval assign (Std.Tactic.BVDecide.BVExpr.replicate n expr h) =
    BitVec.replicate n (Std.Tactic.BVDecide.BVExpr.eval assign expr)
-- Init.Data.Dyadic.Basic
Dyadic.add_zero : ∀ (x : Dyadic), x + 0 = x
-- Lean.PrettyPrinter.Delaborator.Builtins
Lean.PrettyPrinter.Delaborator.delabRoo : Lean.PrettyPrinter.Delaborator.Delab
-- Mathlib.RingTheory.Spectrum.Prime.Jacobson
PrimeSpectrum.instJacobsonSpaceOfIsJacobsonRing : ∀ {R : Type u_1} [inst : CommRing R] [IsJacobsonRing R], JacobsonSpace (PrimeSpectrum R)
-- Mathlib.NumberTheory.ArithmeticFunction.LFunction
/-- The uniform space structure on arithmetic functions is complete.
See `tendsTo_eulerProduct_of_tendsTo` for the outward facing `eulerProduct` API.  -/
ArithmeticFunction.instCompleteSpace : ∀ {R : Type u_2} [inst : CommSemiring R], CompleteSpace (ArithmeticFunction R)
-- Mathlib.Algebra.Module.Projective
Module.Projective.directSum : ∀ {R : Type u} [inst : Semiring R] {ι : Type v} {M : ι → Type w} [inst_1 : (i : ι) → AddCommMonoid (M i)]
  [inst_2 : (i : ι) → Module R (M i)] [∀ (i : ι), Module.Projective R (M i)],
  Module.Projective R (DirectSum ι fun i => M i)
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.contains_inter : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashSet.Raw α} [EquivBEq α] [LawfulHashable α],
  m₁.WF → m₂.WF → ∀ {k : α}, (m₁ ∩ m₂).contains k = (m₁.contains k && m₂.contains k)
-- Mathlib.Algebra.Homology.Embedding.CochainComplex
CochainComplex.isGE_shift : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (K : CochainComplex C ℤ) [CategoryTheory.CategoryWithHomology C] (n : ℤ) [K.IsGE n] (a n' : ℤ),
  a + n' = n → ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K).IsGE n'
-- Init.Data.UInt.Lemmas
UInt64.lt_or_lt_of_ne : ∀ {a b : UInt64}, a ≠ b → a < b ∨ b < a
-- Mathlib.Data.Finsupp.Single
Finsupp.eq_single_iff : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] {f : α →₀ M} {a : α} {b : M},
  (f = fun₀ | a => b) ↔ f.support ⊆ {a} ∧ f a = b
-- Mathlib.GroupTheory.GroupAction.Blocks
/-- The type of blocks for an additive group action containing a given element is a
bounded order.  -/
AddAction.BlockMem.instBoundedOrder : (G : Type u_1) →
  [inst : AddGroup G] → {X : Type u_2} → [inst_1 : AddAction G X] → (a : X) → BoundedOrder (AddAction.BlockMem G a)
-- Mathlib.Data.Sum.Basic
Sum.eq_left_iff_getLeft_eq : ∀ {α : Type u} {β : Type v} {x : α ⊕ β} {a : α}, x = Sum.inl a ↔ ∃ (h : x.isLeft = true), x.getLeft h = a
-- Std.Data.Internal.List.Associative
Std.Internal.List.isEmpty_eq_false_iff_exists_containsKey : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [ReflBEq α] {l : List ((a : α) × β a)},
  l.isEmpty = false ↔ ∃ a, Std.Internal.List.containsKey a l = true
-- Init.Data.List.Sublist
List.suffix_map_iff : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {l₁ : List α} {l₂ : List β},
  l₂ <:+ List.map f l₁ ↔ ∃ l, l <:+ l₁ ∧ l₂ = List.map f l
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.ext_iff : ∀ {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Semiring A₂]
  [inst_3 : Algebra R A₁] [inst_4 : Algebra R A₂] {f g : A₁ ≃ₐ[R] A₂}, f = g ↔ ∀ (a : A₁), f a = g a
-- Lean.Data.Lsp.InitShutdown
Lean.Lsp.InitializeParams.workspaceFolders? : Lean.Lsp.InitializeParams → Option (Array Lean.Lsp.WorkspaceFolder)
-- Mathlib.RingTheory.Localization.NumDen
IsFractionRing.num_mul_den_eq_num_iff_eq' : ∀ {A : Type u_1} [inst : CommRing A] [inst_1 : IsDomain A] [inst_2 : UniqueFactorizationMonoid A] {K : Type u_2}
  [inst_3 : Field K] [inst_4 : Algebra A K] [inst_5 : IsFractionRing A K] {x y : K},
  y * (algebraMap A K) ↑(IsFractionRing.den A x) = (algebraMap A K) (IsFractionRing.num A x) ↔ x = y
-- Mathlib.Topology.Sheaves.Over
TopologicalSpace.Opens.instIsDenseSubsiteOverSubtypeMemOverGrothendieckTopologyFunctorOverEquivalence : ∀ {X : Type u} [inst : TopologicalSpace X] (U : TopologicalSpace.Opens X),
  CategoryTheory.Functor.IsDenseSubsite ((Opens.grothendieckTopology X).over U) (Opens.grothendieckTopology ↥U)
    U.overEquivalence.functor
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.degree_pow_le : ∀ {R : Type u} [inst : Semiring R] (p : Polynomial R) (n : ℕ), (p ^ n).degree ≤ n • p.degree
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.map_f₁₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  (sq : CategoryTheory.Square C) (F : CategoryTheory.Functor C D), (sq.map F).f₁₂ = F.map sq.f₁₂
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
LinearIndependent.neg : ∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {v : ι → M}, LinearIndependent R v → LinearIndependent R (-v)
-- Mathlib.CategoryTheory.Discrete.Basic
/-- `Discrete α` is equivalent to the original type `α`.  -/
CategoryTheory.discreteEquiv : {α : Type u₁} → CategoryTheory.Discrete α ≃ α
-- Lean.Elab.Tactic.BuiltinTactic
/-- Performs an `intro` step.
- `nref` is a ref for the introduced hypothesis
- `n` is the name to use for the introduced hypothesis, `_` means to use a hygienic name
  and `rfl` means to use a hygienic name and `subst`
- `typeStx?` is used to change the type of the introduced hypothesis
 -/
_private.Lean.Elab.Tactic.BuiltinTactic.0.Lean.Elab.Tactic.evalIntro.introStep : Lean.Syntax → Lean.Name → optParam (Option Lean.Syntax) none → Lean.Elab.Tactic.TacticM Unit
-- Mathlib.CategoryTheory.Monoidal.Bimod
Bimod.TensorBimod.actRight_one' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Limits.HasCoequalizers C] {R S T : CategoryTheory.Mon C} (P : Bimod R S) (Q : Bimod S T)
  [inst_3 :
    ∀ (X : C),
      CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁}
        (CategoryTheory.MonoidalCategory.tensorRight X)],
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (Bimod.TensorBimod.X P Q) CategoryTheory.MonObj.one)
      (Bimod.TensorBimod.actRight P Q) =
    (CategoryTheory.MonoidalCategoryStruct.rightUnitor (Bimod.TensorBimod.X P Q)).hom
-- Lean.Parser.Extension
Lean.Parser.ParserExtension : Type
-- Mathlib.Topology.EMetricSpace.VariationOnFromTo
variationOnFromTo.sub_left : ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] {f : α → E} {s : Set α},
  LocallyBoundedVariationOn f s →
    ∀ {a b c : α},
      a ∈ s → b ∈ s → c ∈ s → variationOnFromTo f s a b - variationOnFromTo f s c b = variationOnFromTo f s a c
-- Mathlib.Topology.Inseparable
SeparationQuotient.instSubsingletonOfIndiscreteTopology : ∀ {α : Type u_4} [inst : TopologicalSpace α] [IndiscreteTopology α], Subsingleton (SeparationQuotient α)
-- Mathlib.RingTheory.RingHom.StandardSmooth
RingHom.IsStandardSmoothOfRelativeDimension.isStandardSmooth : ∀ (n : ℕ) {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
  RingHom.IsStandardSmoothOfRelativeDimension n f → f.IsStandardSmooth
-- Init.Grind.AC
Lean.Grind.AC.Seq.insert : Lean.Grind.AC.Var → Lean.Grind.AC.Seq → Lean.Grind.AC.Seq
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
MeasurableEquiv.refl_apply : ∀ (α : Type u_6) [inst : MeasurableSpace α] (a : α), (MeasurableEquiv.refl α) a = a
-- Mathlib.Algebra.Ring.Divisibility.Lemmas
Commute.pow_dvd_sub_pow_of_pow_eq_zero_right : ∀ {R : Type u_1} {x y : R} {n m p : ℕ} [inst : Ring R], n + m ≤ p + 1 → Commute x y → y ^ n = 0 → x ^ m ∣ (x - y) ^ p
-- Std.Sync.CancellationContext
Std.CancellationContext.id : Std.CancellationContext → UInt64
-- Mathlib.MeasureTheory.SetSemiring
MeasureTheory.IsSetSemiring.disjoint_sUnion_disjointOfDiffUnion : ∀ {α : Type u_1} {C : Set (Set α)} {s : Set α} {I : Finset (Set α)} (hC : MeasureTheory.IsSetSemiring C) (hs : s ∈ C)
  (hI : ↑I ⊆ C), Disjoint (⋃₀ ↑I) (⋃₀ ↑(hC.disjointOfDiffUnion hs hI))
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.biproduct.ι_matrix_assoc : ∀ {J : Type} [inst : Finite J] {K : Type} [inst_1 : Finite K] {C : Type u} [inst_2 : CategoryTheory.Category.{v, u} C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_4 : CategoryTheory.Limits.HasFiniteBiproducts C] {f : J → C}
  {g : K → C} (m : (j : J) → (k : K) → f j ⟶ g k) (j : J) {Z : C} (h : ⨁ g ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι f j)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.matrix m) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.lift fun k => m j k) h
-- Mathlib.NumberTheory.Divisors
Nat.prod_div_divisors : ∀ {α : Type u_1} [inst : CommMonoid α] (n : ℕ) (f : ℕ → α), ∏ d ∈ n.divisors, f (n / d) = n.divisors.prod f
-- Mathlib.Order.Defs.PartialOrder
/-- **Alias** of `ge_antisymm`. -/
eq_of_ge_of_le : ∀ {α : Type u_1} [inst : PartialOrder α] {a b : α}, b ≤ a → a ≤ b → a = b
-- Mathlib.LinearAlgebra.AffineSpace.Basis
AffineBasis.tot' : ∀ {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} [inst : AddCommGroup V] [inst_1 : AddTorsor V P]
  [inst_2 : Ring k] [inst_3 : Module k V] (self : AffineBasis ι k P), affineSpan k (Set.range self.toFun) = ⊤
-- Mathlib.CategoryTheory.Abelian.Injective.Extend
CategoryTheory.InjectiveResolution.Hom.ι'_comp_hom'_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X : C}
  {R : CategoryTheory.InjectiveResolution X} {X' : C} {R' : CategoryTheory.InjectiveResolution X'} {f : X ⟶ X'}
  (φ : R.Hom R' f) {Z : CochainComplex C ℤ} (h : R'.cochainComplex ⟶ Z),
  CategoryTheory.CategoryStruct.comp R.ι' (CategoryTheory.CategoryStruct.comp φ.hom' h) =
    CategoryTheory.CategoryStruct.comp ((CochainComplex.singleFunctor C 0).map f)
      (CategoryTheory.CategoryStruct.comp R'.ι' h)
-- Mathlib.RingTheory.Extension.Basic
Algebra.Extension.Cotangent.mk_surjective : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  {P : Algebra.Extension R S}, Function.Surjective ⇑Algebra.Extension.Cotangent.mk
-- Std.Data.DTreeMap.Internal.Queries
/-- Returns an `Array` of the key/value pairs in order.  -/
Std.DTreeMap.Internal.Impl.toArray : {α : Type u} → {β : α → Type v} → Std.DTreeMap.Internal.Impl α β → Array ((a : α) × β a)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.InlayHintClientCapabilities.mk.inj : ∀ {dynamicRegistration? : Option Bool} {resolveSupport? : Option Lean.Lsp.ResolveSupport}
  {dynamicRegistration?_1 : Option Bool} {resolveSupport?_1 : Option Lean.Lsp.ResolveSupport},
  { dynamicRegistration? := dynamicRegistration?, resolveSupport? := resolveSupport? } =
      { dynamicRegistration? := dynamicRegistration?_1, resolveSupport? := resolveSupport?_1 } →
    dynamicRegistration? = dynamicRegistration?_1 ∧ resolveSupport? = resolveSupport?_1
-- Mathlib.Algebra.Order.Field.GeomSum
geom_sum_lt : ∀ {K : Type u_1} [inst : Semifield K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] [CanonicallyOrderedAdd K]
  [inst_4 : Sub K] [OrderedSub K] {x : K}, x ≠ 0 → x < 1 → ∀ (n : ℕ), ∑ i ∈ Finset.range n, x ^ i < (1 - x)⁻¹
-- Mathlib.GroupTheory.Divisible
Prod.rootableBy : {β : Type u_3} →
  {B : Type u_4} →
    {B' : Type u_5} →
      [inst : Pow B β] →
        [inst_1 : Pow B' β] →
          [inst_2 : Zero β] →
            [inst_3 : Monoid B] → [inst_4 : Monoid B'] → [RootableBy B β] → [RootableBy B' β] → RootableBy (B × B') β
-- Std.Data.HashSet.Lemmas
Std.HashSet.get!_eq_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [LawfulBEq α] [inst : Inhabited α] {k : α},
  k ∈ m → m.get! k = k
-- Mathlib.Data.Nat.Digits.Defs
Nat.ofDigits.eq_1 : ∀ {α : Type u_1} [inst : Semiring α] (b : α), Nat.ofDigits b [] = 0
-- Mathlib.Algebra.ContinuedFractions.Basic
GenContFract.instInhabitedPair : {a : Type u_2} → [Inhabited a] → Inhabited (GenContFract.Pair a)
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
CategoryTheory.Oplax.LaxTrans.instInhabited : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F : CategoryTheory.OplaxFunctor B C} → Inhabited (CategoryTheory.Oplax.LaxTrans F F)
-- Mathlib.CategoryTheory.ConcreteCategory.Forget
/-- **Alias** of `CategoryTheory.ConcreteCategory.forget_map_eq_ofHom`. -/
CategoryTheory.ConcreteCategory.forget_map_eq_coe : ∀ {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] {X Y : C} (f : X ⟶ Y),
  (CategoryTheory.forget C).map f = TypeCat.ofHom ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Std.Sat.AIG.CachedLemmas
/-- The central equality theorem between `mkGateCached` and `mkGate`.
 -/
Std.Sat.AIG.mkGateCached_eval_eq_mkGate_eval : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {assign : α → Bool} {aig : Std.Sat.AIG α}
  {input : aig.BinaryInput}, ⟦assign, aig.mkGateCached input⟧ = ⟦assign, aig.mkGate input⟧
-- Mathlib.RingTheory.Valuation.Quotient
/-- If `hJ : J ⊆ supp v` then `onQuotVal hJ` is the induced function on `R / J` as a function.
Note: it's just the function; the valuation is `onQuot hJ`.  -/
AddValuation.onQuotVal : {R : Type u_1} →
  {Γ₀ : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : LinearOrderedAddCommMonoidWithTop Γ₀] →
        (v : AddValuation R Γ₀) → {J : Ideal R} → J ≤ v.supp → R ⧸ J → Γ₀
-- Mathlib.Analysis.CStarAlgebra.Module.Synonym
WithCStarModule.add_fst : ∀ {A : Type u_2} {E : Type u_3} {F : Type u_4} (x y : WithCStarModule A (E × F)) [inst : AddCommGroup E]
  [inst_1 : AddCommGroup F], (x + y).1 = x.1 + y.1
-- Mathlib.LinearAlgebra.Matrix.Kronecker
Matrix.kronecker_ofNat : ∀ {α : Type u_3} {l : Type u_9} {m : Type u_10} {n : Type u_11} [inst : NonAssocSemiring α] [inst_1 : DecidableEq n]
  (A : Matrix l m α) (b : ℕ) [inst_2 : b.AtLeastTwo],
  Matrix.kroneckerMap (fun x1 x2 => x1 * x2) A (OfNat.ofNat b) =
    Matrix.blockDiagonal fun x => MulOpposite.op (OfNat.ofNat b) • A
-- Mathlib.Data.DFinsupp.BigOperators
DFinsupp.sumAddHom_comp_single : ∀ {ι : Type u} {γ : Type w} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → AddZeroClass (β i)]
  [inst_2 : AddCommMonoid γ] (f : (i : ι) → β i →+ γ) (i : ι),
  (DFinsupp.sumAddHom f).comp (DFinsupp.singleAddHom β i) = f i
-- Mathlib.RingTheory.Ideal.Operations
Ideal.subset_union_prime' : ∀ {ι : Type u_1} {R : Type u} [inst : CommRing R] {s : Finset ι} {f : ι → Ideal R} {a b : ι},
  (∀ i ∈ s, (f i).IsPrime) →
    ∀ {I : Ideal R}, ↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ i ∈ ↑s, ↑(f i) ↔ I ≤ f a ∨ I ≤ f b ∨ ∃ i ∈ s, I ≤ f i
-- Mathlib.GroupTheory.GroupAction.IterateAct
IterateAddAct.mk.injEq : ∀ {α : Type u_1} {f : α → α} (val val_1 : ℕ), ({ val := val } = { val := val_1 }) = (val = val_1)
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.Scheme.Opens.toSpecΓ_SpecMap_presheaf_map_assoc : ∀ {X : AlgebraicGeometry.Scheme} (U V : X.Opens) (h : U ≤ V) {Z : AlgebraicGeometry.Scheme}
  (h_1 : AlgebraicGeometry.Spec (X.presheaf.obj (Opposite.op V)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp U.toSpecΓ
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (X.presheaf.map (CategoryTheory.homOfLE h).op))
        h_1) =
    CategoryTheory.CategoryStruct.comp (X.homOfLE h) (CategoryTheory.CategoryStruct.comp V.toSpecΓ h_1)
-- Mathlib.Algebra.Ring.Commute
Commute.sub_left : ∀ {R : Type u} [inst : NonUnitalNonAssocRing R] {a b c : R}, Commute a c → Commute b c → Commute (a - b) c
-- Mathlib.Geometry.Euclidean.SignedDist
signedDist_triangle : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (v : V) (p q r : P), ((signedDist v) p) q + ((signedDist v) q) r = ((signedDist v) p) r
-- Lean.Parser.Do
Lean.Parser.Term.dependentParam : Lean.Parser.Parser
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
/-- A compact subset has finite measure for a measure which is finite on compacts.  -/
IsCompact.measure_lt_top : ∀ {α : Type u_1} {m0 : MeasurableSpace α} [inst : TopologicalSpace α] {μ : MeasureTheory.Measure α}
  [MeasureTheory.IsFiniteMeasureOnCompacts μ] ⦃K : Set α⦄, IsCompact K → μ K < ⊤
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instNonAssocSemiring : {α : Type u_1} → {l : Filter α} → {R : Type u_5} → [NonAssocSemiring R] → NonAssocSemiring (l.Germ R)
-- Mathlib.MeasureTheory.Measure.Map
MeasureTheory.Measure.mapₗ_congr : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α}
  {f g : α → β},
  Measurable f → Measurable g → f =ᵐ[μ] g → (MeasureTheory.Measure.mapₗ f) μ = (MeasureTheory.Measure.mapₗ g) μ
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
/-- For subgraphs `G₁`, `G₂`, `G₁ ≤ G₂` iff `G₁.verts ⊆ G₂.verts` and
`∀ a b, G₁.adj a b → G₂.adj a b`.  -/
SimpleGraph.Subgraph.instPartialOrder : {V : Type u} → {G : SimpleGraph V} → PartialOrder G.Subgraph
-- Lean.Elab.Tactic.BuiltinTactic
Lean.Elab.Tactic.evalChoiceAux : Array Lean.Syntax → ℕ → Lean.Elab.Tactic.TacticM Unit
-- Mathlib.CategoryTheory.Linear.LinearFunctor
CategoryTheory.Functor.mapLinearMap_apply : ∀ (R : Type u_1) [inst : Semiring R] {C : Type u_2} {D : Type u_3} [inst_1 : CategoryTheory.Category.{v_1, u_2} C]
  [inst_2 : CategoryTheory.Category.{v_2, u_3} D] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : CategoryTheory.Preadditive D] [inst_5 : CategoryTheory.Linear R C] [inst_6 : CategoryTheory.Linear R D]
  (F : CategoryTheory.Functor C D) [inst_7 : CategoryTheory.Functor.Linear R F] [inst_8 : F.Additive] {X Y : C}
  (a : X ⟶ Y), (CategoryTheory.Functor.mapLinearMap R F) a = (↑F.mapAddHom).toFun a
-- Mathlib.RingTheory.MvPowerSeries.Restricted
MvPowerSeries.isRestricted_C : ∀ {R : Type u_1} [inst : NormedRing R] {σ : Type u_2} (c : σ → ℝ) (a : R),
  MvPowerSeries.IsRestricted c (MvPowerSeries.C a)
-- Mathlib.LinearAlgebra.AffineSpace.Basis
AffineBasis.coord_apply_centroid : ∀ {ι : Type u_1} {k : Type u_5} {V : Type u_6} {P : Type u_7} [inst : AddCommGroup V] [inst_1 : AddTorsor V P]
  [inst_2 : DivisionRing k] [inst_3 : Module k V] [CharZero k] (b : AffineBasis ι k P) {s : Finset ι} {i : ι},
  i ∈ s → (b.coord i) (Finset.centroid k s ⇑b) = (↑s.card)⁻¹
-- Mathlib.Topology.Homeomorph.Defs
Homeomorph.image_interior : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (h : X ≃ₜ Y) (s : Set X),
  ⇑h '' interior s = interior (⇑h '' s)
-- Lean.Elab.ConfigEval.DeriveEvalTerm
_private.Lean.Elab.ConfigEval.DeriveEvalTerm.0.Lean.Elab.ConfigEval.ensureEvalTerm.useCtor : Lean.InductiveVal → Lean.Name → Bool
-- Init.Data.Vector.Lemmas
Vector.isPrefixOf.eq_1 : ∀ {α : Type u_1} {m n : ℕ} [inst : BEq α] (xs : Vector α m) (ys : Vector α n),
  xs.isPrefixOf ys = xs.toArray.isPrefixOf ys.toArray
-- Mathlib.Analysis.CStarAlgebra.CompletelyPositiveMap
/-- Notation for a `CompletelyPositiveMap`.  -/
CStarAlgebra.«term_→CP_» : Lean.TrailingParserDescr
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.of_toArray_perm : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp},
  t₁.toArray.Perm t₂.toArray → t₁.Equiv t₂
-- Mathlib.Analysis.Normed.Group.Constructions
OrderDual.seminormedCommGroup : {E : Type u_2} → [SeminormedCommGroup E] → SeminormedCommGroup Eᵒᵈ
-- Mathlib.Probability.Distributions.Gamma
/-- The gamma pdf is measurable.  -/
ProbabilityTheory.measurable_gammaPDFReal : ∀ (a r : ℝ), Measurable (ProbabilityTheory.gammaPDFReal a r)
-- Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Filter.Tendsto.nnrpow : ∀ {α : Type u_1} {f : Filter α} {u : α → NNReal} {v : α → ℝ} {x : NNReal} {y : ℝ},
  Filter.Tendsto u f (nhds x) →
    Filter.Tendsto v f (nhds y) → x ≠ 0 ∨ 0 < y → Filter.Tendsto (fun a => u a ^ v a) f (nhds (x ^ y))
-- Mathlib.Algebra.Ring.Action.Basic
/-- Typeclass for multiplicative actions by monoids on semirings.

This combines `DistribMulAction` with `MulDistribMulAction`: it expresses
the interplay between the action and both addition and multiplication on the target.
Two key axioms are `g • (x + y) = (g • x) + (g • y)` and `g • (x * y) = (g • x) * (g • y)`.

A typical use case is the action of a Galois group $Gal(L/K)$ on the field `L`.
 -/
MulSemiringAction : (M : Type u) → (R : Type v) → [Monoid M] → [Semiring R] → Type (max u v)
-- Mathlib.Topology.Homeomorph.Defs
Homeomorph.image_symm : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (h : X ≃ₜ Y),
  Set.image ⇑h.symm = Set.preimage ⇑h
-- Mathlib.Probability.Process.Adapted
MeasureTheory.Adapted.inv : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] {f : MeasureTheory.Filtration ι m}
  {β : ι → Type u_3} [inst_1 : (i : ι) → MeasurableSpace (β i)] {u : (i : ι) → Ω → β i} [inst_2 : (i : ι) → Group (β i)]
  [∀ (i : ι), MeasurableInv (β i)], MeasureTheory.Adapted f u → MeasureTheory.Adapted f u⁻¹
-- Mathlib.NumberTheory.Niven
/-- `tan(q * π)` for `q : ℚ` is algebraic over `ℤ`, using the real `tan` function.  -/
Real.isAlgebraic_tan_rat_mul_pi : ∀ (q : ℚ), IsAlgebraic ℤ (Real.tan (↑q * Real.pi))
-- Mathlib.Analysis.Normed.Module.Basic
Metric.diam_ball_eq : ∀ {E : Type u_6} [inst : NormedAddCommGroup E] [NormedSpace ℝ E] [Nontrivial E] (x : E) {r : ℝ},
  0 ≤ r → Metric.diam (Metric.ball x r) = 2 * r
-- Std.Do.Triple.SpecLemmas
_private.Std.Do.Triple.SpecLemmas.0.Std.Do.WhileVariant.add_eval : ∀ {α : Type u} {ps : Std.Do.PostShape} {P Q : Std.Do.SPred ps.args} (variant : Std.Do.WhileVariant α ps) (a : α),
  ((∃ m, variant.eval a m ∧ P) ⊢ₛ Q) → P ⊢ₛ Q
-- Mathlib.Analysis.SpecialFunctions.Exp
/-- `Complex.exp z → 0` as `Complex.re z → -∞`.  -/
Complex.tendsto_exp_comap_re_atBot : Filter.Tendsto Complex.exp (Filter.comap Complex.re Filter.atBot) (nhds 0)
-- Mathlib.LinearAlgebra.TensorProduct.Map
/-- `rTensorHom M` is the natural linear map that sends a linear map `f : N →ₗ P` to `f ⊗ M`.

See also `Module.End.rTensorAlgHom`.  -/
LinearMap.rTensorHom : {R : Type u_1} →
  [inst : CommSemiring R] →
    (M : Type u_7) →
      {N : Type u_8} →
        {P : Type u_9} →
          [inst_1 : AddCommMonoid M] →
            [inst_2 : AddCommMonoid N] →
              [inst_3 : AddCommMonoid P] →
                [inst_4 : Module R M] →
                  [inst_5 : Module R N] →
                    [inst_6 : Module R P] → (N →ₗ[R] P) →ₗ[R] TensorProduct R N M →ₗ[R] TensorProduct R P M
-- Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms
CategoryTheory.ObjectProperty.instIsClosedUnderIsomorphismsIsoClosure : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C),
  P.isoClosure.IsClosedUnderIsomorphisms
-- Init.Tactics
/-- The `dsimp` tactic is the definitional simplifier. It is similar to `simp` but only
applies theorems that hold by reflexivity. Thus, the result is guaranteed to be
definitionally equal to the input.
 -/
Lean.Parser.Tactic.dsimp : Lean.ParserDescr