mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
/-- The interval integral `∫ x in a..b, f x` is defined
as `∫ x in Ioc a b, f x - ∫ x in Ioc b a, f x`. If `a ≤ b`, then it equals
`∫ x in Ioc a b, f x`, otherwise it equals `-∫ x in Ioc b a, f x`.  -/
«term∫_In_.._,_» : Lean.ParserDescr
-- Std.Do.WP.Monad
Std.Do.OptionT.instWPMonad : {m : Type u → Type v} →
  {ps : Std.Do.PostShape} →
    [inst : Monad m] → [Std.Do.WPMonad m ps] → Std.Do.WPMonad (OptionT m) (Std.Do.PostShape.except PUnit.{u + 1} ps)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.getD_diff_of_not_mem_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {k : α} {fallback : β}, k ∉ m₁ → Std.DHashMap.Const.getD (m₁.diff m₂) k fallback = fallback
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Free
/-- The inclusions `unit R ⟶ free I`.  -/
SheafOfModules.ιFree : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {R : CategoryTheory.Sheaf J RingCat} →
        [inst_1 : CategoryTheory.HasWeakSheafify J AddCommGrpCat] →
          [inst_2 : J.WEqualsLocallyBijective AddCommGrpCat] →
            {I : Type u} → I → (SheafOfModules.unit R ⟶ SheafOfModules.free I)
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
/-- A finite product of antitone functions is antitone.  -/
Antitone.finsetProd' : ∀ {ι : Type u_1} {N : Type u_5} [inst : CommMonoid N] [inst_1 : Preorder N] {s : Finset ι} [MulLeftMono N]
  {γ : Type u_9} [inst_3 : Preorder γ] {f : ι → γ → N}, (∀ i ∈ s, Antitone (f i)) → Antitone fun x => ∏ i ∈ s, f i x
-- Mathlib.Order.Hom.Lattice
SupHom.instBoundedOrder.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : Max α] [inst_1 : SemilatticeSup β] [inst_2 : BoundedOrder β],
  SupHom.instBoundedOrder = BoundedOrder.lift DFunLike.coe ⋯ ⋯ ⋯
-- Mathlib.RepresentationTheory.Character
Representation.char_linHom : ∀ {G : Type u_1} {k : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Group G] [inst_1 : Field k]
  [inst_2 : AddCommGroup V] [inst_3 : Module k V] [FiniteDimensional k V] [inst_5 : AddCommGroup W]
  [inst_6 : Module k W] [FiniteDimensional k W] (ρ : Representation k G V) (σ : Representation k G W) (g : G),
  (ρ.linHom σ).character g = ρ.character g⁻¹ * σ.character g
-- Init.Data.SInt.Lemmas
Int16.toInt32_ofNat : ∀ {n : ℕ}, n ≤ 32767 → (OfNat.ofNat n).toInt32 = OfNat.ofNat n
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F.op : Cᵒᵖ ⥤ Dᵒᵖ` preserves colimits of shape `Jᵒᵖ`, then `F : C ⥤ D` preserves limits
of shape `J`.  -/
CategoryTheory.Limits.preservesLimitsOfShape_of_op : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (J : Type w) [inst_2 : CategoryTheory.Category.{w', w} J] (F : CategoryTheory.Functor C D)
  [CategoryTheory.Limits.PreservesColimitsOfShape Jᵒᵖ F.op], CategoryTheory.Limits.PreservesLimitsOfShape J F
-- Mathlib.CategoryTheory.Monoidal.Bimon_
CategoryTheory.Bimon.instIsComonHomHomEquivMonComonCounitIsoAppXAux : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (M : CategoryTheory.Mon (CategoryTheory.Comon C)),
  CategoryTheory.IsComonHom (CategoryTheory.Bimon.equivMonComonCounitIsoAppXAux M).hom
-- Mathlib.GroupTheory.GroupAction.Basic
/-- To prove inclusion of a *subgroup* in a stabilizer, it is enough to prove inclusions.  -/
MulAction.le_stabilizer_iff_smul_le : ∀ {G : Type u_1} [inst : Group G] {α : Type u_2} [inst_1 : MulAction G α] (s : Set α) (H : Subgroup G),
  H ≤ MulAction.stabilizer G s ↔ ∀ g ∈ H, g • s ⊆ s
-- Mathlib.CategoryTheory.Subobject.FactorThru
CategoryTheory.Subobject.factorThru_arrow_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (P : CategoryTheory.Subobject Y) (f : X ⟶ Y)
  (h : P.Factors f) {Z : C} (h_1 : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (P.factorThru f h) (CategoryTheory.CategoryStruct.comp P.arrow h_1) =
    CategoryTheory.CategoryStruct.comp f h_1
-- Mathlib.CategoryTheory.Limits.Connected
CategoryTheory.Limits.constCocone_pt : ∀ (J : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} C]
  (X : C), (CategoryTheory.Limits.constCocone J X).pt = X
-- Lean.Util.FindLevelMVar
Lean.FindLevelMVar.mainLevel : (Lean.LMVarId → Bool) → Lean.Level → Lean.FindLevelMVar.Visitor
-- Mathlib.CategoryTheory.Triangulated.SpectralObject
CategoryTheory.Triangulated.SpectralObject.ω₂_obj_mor₁ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Limits.HasZeroObject C]
  [inst_3 : CategoryTheory.HasShift C ℤ] [inst_4 : CategoryTheory.Preadditive C]
  [inst_5 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_6 : CategoryTheory.Pretriangulated C]
  (X : CategoryTheory.Triangulated.SpectralObject C ι) (j : CategoryTheory.ComposableArrows ι 2),
  (X.ω₂.obj j).mor₁ =
    X.ω₁.map
      (CategoryTheory.ComposableArrows.homMk₁ (CategoryTheory.CategoryStruct.id (j.obj 0))
        (j.map (CategoryTheory.homOfLE ⋯)) ⋯)
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.mul_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : Mul β]
  [inst_3 : ContinuousMul β] (f g : C(α, β)) (x : α), (f * g) x = f x * g x
-- Aesop.Options.Public
Aesop.instReprOptions.repr : Aesop.Options → ℕ → Std.Format
-- Mathlib.Probability.Kernel.Composition.CompMap
ProbabilityTheory.Kernel.map_comp : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {δ : Type u_5}
  {mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ} (κ : ProbabilityTheory.Kernel α β)
  (η : ProbabilityTheory.Kernel β γ) (f : γ → δ), (η.comp κ).map f = (η.map f).comp κ
-- Mathlib.Analysis.InnerProductSpace.Rayleigh
/-- The *Rayleigh quotient* of a continuous linear map `T` (over `ℝ` or `ℂ`) at a vector `x` is
the quantity `re ⟪T x, x⟫ / ‖x‖ ^ 2`.  -/
ContinuousLinearMap.rayleighQuotient : {𝕜 : Type u_1} →
  [inst : RCLike 𝕜] →
    {E : Type u_2} → [inst_1 : NormedAddCommGroup E] → [inst_2 : InnerProductSpace 𝕜 E] → (E →L[𝕜] E) → E → ℝ
-- Mathlib.Data.Multiset.ZeroCons
/-- `cons a s` is the multiset which contains `s` plus one more instance of `a`.  -/
Multiset.cons : {α : Type u_1} → α → Multiset α → Multiset α
-- Mathlib.Data.Set.Basic
Set.powerset_empty : ∀ {α : Type u}, 𝒫 ∅ = {∅}
-- Mathlib.Data.Finset.Pi
Set.piCongrLeft_comp_domRestrict : ∀ {ι : Type u_2} {π : ι → Type u_3} {s : Finset ι},
  ⇑(Equiv.piCongrLeft (fun i => π ↑i) s.equivToSet.symm) ∘ (↑s).domRestrict = s.restrict
-- Aesop.RuleTac.Basic
Aesop.CasesTarget.decl : Lean.Name → Aesop.CasesTarget
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Presieve.FunctorPushforwardStructure.mk.injEq : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {X : C} {S : CategoryTheory.Presieve X} {Y : D} {f : Y ⟶ F.obj X} (preobj : C)
  (premap : preobj ⟶ X) (lift : Y ⟶ F.obj preobj) (cover : S premap)
  (fac : f = CategoryTheory.CategoryStruct.comp lift (F.map premap)) (preobj_1 : C) (premap_1 : preobj_1 ⟶ X)
  (lift_1 : Y ⟶ F.obj preobj_1) (cover_1 : S premap_1)
  (fac_1 : f = CategoryTheory.CategoryStruct.comp lift_1 (F.map premap_1)),
  ({ preobj := preobj, premap := premap, lift := lift, cover := cover, fac := fac } =
      { preobj := preobj_1, premap := premap_1, lift := lift_1, cover := cover_1, fac := fac_1 }) =
    (preobj = preobj_1 ∧ premap ≍ premap_1 ∧ lift ≍ lift_1)
-- Init.Core
Function.false_comp : ∀ {α : Sort u_1} {β : Sort u_2} {f : α → β}, (fun x => false) ∘ f = fun x => false
-- Mathlib.Data.Set.Lattice
/-- A reversed version of `iUnion_psigma` with a curried map.  -/
Set.iUnion_psigma' : ∀ {α : Type u_1} {β : Type u_2} {γ : α → Type u_12} (s : (i : α) → γ i → Set β), ⋃ i, ⋃ a, s i a = ⋃ ia, s ia.fst ia.snd
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKeyD_eq_getKey? : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {l : List ((a : α) × β a)} {a fallback : α},
  Std.Internal.List.getKeyD a l fallback = (Std.Internal.List.getKey? a l).getD fallback
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.LeftExtension.postcomp₁_obj_right_obj : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} {D' : Type u_5} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  [inst_3 : CategoryTheory.Category.{v_5, u_5} D'] {L : CategoryTheory.Functor C D} {L' : CategoryTheory.Functor C D'}
  (G : CategoryTheory.Functor D D') (f : L' ⟶ L.comp G) (F : CategoryTheory.Functor C H)
  (X :
    CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit F) ((CategoryTheory.Functor.whiskeringLeft C D' H).obj L'))
  (X_1 : D), ((CategoryTheory.Functor.LeftExtension.postcomp₁ G f F).obj X).right.obj X_1 = X.right.obj (G.obj X_1)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.constMaxEntry_eq : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t₁ t₂ : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  t₁.WF →
    t₂.WF →
      ∀ (h : t₁.Equiv t₂) {he : t₁.isEmpty = false},
        Std.DTreeMap.Internal.Impl.Const.maxEntry t₁ he = Std.DTreeMap.Internal.Impl.Const.maxEntry t₂ ⋯
-- Mathlib.Probability.Process.Adapted
/-- **Alias** of `MeasureTheory.IsStronglyProgressive.finsetProd`. -/
MeasureTheory.ProgMeasurable.finset_prod : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] {f : MeasureTheory.Filtration ι m}
  {β : Type u_3} [inst_1 : TopologicalSpace β] [inst_2 : MeasurableSpace ι] {γ : Type u_4} [inst_3 : CommMonoid β]
  [ContinuousMul β] {U : γ → ι → Ω → β} {s : Finset γ},
  (∀ c ∈ s, MeasureTheory.IsStronglyProgressive f (U c)) →
    MeasureTheory.IsStronglyProgressive f fun i a => ∏ c ∈ s, U c i a
-- Mathlib.MeasureTheory.Covering.Besicovitch
Besicovitch.TauPackage.mk.sizeOf_spec : ∀ {β : Type u_1} {α : Type u_2} [inst : SizeOf β] [inst_1 : SizeOf α] (toBallPackage : Besicovitch.BallPackage β α)
  (τ : ℝ) (one_lt_tau : 1 < τ),
  sizeOf { toBallPackage := toBallPackage, τ := τ, one_lt_tau := one_lt_tau } =
    1 + sizeOf toBallPackage + sizeOf τ + sizeOf one_lt_tau
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
/-- The set of pairs of integers congruent to `a` mod `N` and with `gcd` equal to `r`.  -/
EisensteinSeries.gammaSet : (N : ℕ) → ℕ → (Fin 2 → ZMod N) → Set (Fin 2 → ℤ)
-- Lean.Meta.AppBuilder
/-- If `a` and `b` have definitionally equal types, returns `a = b`, otherwise returns `a ≍ b`.
 -/
Lean.Meta.mkEqHEq : Lean.Expr → Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Topology.Algebra.WithZeroTopology
/-- If `γ` is an invertible element of a linearly ordered group with zero element adjoined, then
`Iio (γ : Γ₀)` is a neighbourhood of `0`.  -/
WithZeroTopology.nhds_zero_of_units : ∀ {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] (γ : Γ₀ˣ), Set.Iio ↑γ ∈ nhds 0
-- Mathlib.Order.Interval.Finset.Basic
Finset.Ioo_filter_lt : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : LocallyFiniteOrder α] (a b c : α),
  {x ∈ Finset.Ioo a b | x < c} = Finset.Ioo a (min b c)
-- Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
CategoryTheory.Functor.additive_of_full_essSurj_comp : ∀ {C : Type u_1} {D : Type u_2} {E : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  [inst_3 : CategoryTheory.Preadditive C] [inst_4 : CategoryTheory.Preadditive D]
  [inst_5 : CategoryTheory.Preadditive E] (F : CategoryTheory.Functor C D) [F.Additive] [F.Full] [F.EssSurj]
  (G : CategoryTheory.Functor D E) [(F.comp G).Additive], G.Additive
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.CoconeMorphism.hom_inv_id_assoc : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {c d : CategoryTheory.Limits.Cocone F} (f : c ≅ d) {Z : C} (h : c.pt ⟶ Z),
  CategoryTheory.CategoryStruct.comp f.hom.hom (CategoryTheory.CategoryStruct.comp f.inv.hom h) = h
-- Mathlib.Algebra.GroupWithZero.Basic
mul_ne_zero : ∀ {M₀ : Type u_1} [inst : Mul M₀] [inst_1 : Zero M₀] [NoZeroDivisors M₀] {a b : M₀}, a ≠ 0 → b ≠ 0 → a * b ≠ 0
-- Lean.Meta.Tactic.Simp.Simproc
Lean.Meta.Simp.addSimprocBuiltinAttr : Lean.Name → Bool → Lean.Meta.Simp.Simproc ⊕ Lean.Meta.Simp.DSimproc → IO Unit
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
/-- A morphism in `Over X` from the chosen pullback along `g` of `f` to `Over.mk g`.  -/
CategoryTheory.ChosenPullbacksAlong.snd' : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {Y Z X : C} →
      (f : Y ⟶ X) →
        (g : Z ⟶ X) →
          [inst_1 : CategoryTheory.ChosenPullbacksAlong g] →
            (CategoryTheory.Over.map g).obj
                ((CategoryTheory.ChosenPullbacksAlong.pullback g).obj (CategoryTheory.Over.mk f)) ⟶
              CategoryTheory.Over.mk g
-- Mathlib.RingTheory.Extension.Cotangent.Basis
/-- `T = R[X₁, ..., Xₙ] / (b₁, ..., bᵣ)` where the `bᵢ` are lifts of the basis elements
of `I/I²` in `I`.  -/
_private.Mathlib.RingTheory.Extension.Cotangent.Basis.0.Algebra.Generators.PresentationOfFreeCotangent.Aux.T : {R : Type u_1} →
  {S : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          {ι : Type u_4} →
            {P : Algebra.Generators R S ι} →
              {σ : Type u_5} →
                {b : Module.Basis σ S P.toExtension.Cotangent} →
                  Algebra.Generators.PresentationOfFreeCotangent.Aux✝ P b → Type (max u_1 u_4)
-- Mathlib.CategoryTheory.Subobject.MonoOver
CategoryTheory.MonoOver.mk_arrow : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X A : C} (f : A ⟶ X) [inst_1 : CategoryTheory.Mono f],
  (CategoryTheory.MonoOver.mk f).arrow = f
-- Mathlib.Order.Interval.Finset.Fin
Fin.map_finCongr_Icc : ∀ {n m : ℕ} (h : n = m) (i j : Fin n),
  Finset.map (finCongr h).toEmbedding (Finset.Icc i j) = Finset.Icc (Fin.cast h i) (Fin.cast h j)
-- Mathlib.MeasureTheory.VectorMeasure.Integral
MeasureTheory.VectorMeasure.integral_of_not_completeSpace : ∀ {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G]
  [inst_5 : NormedSpace ℝ G] {μ : MeasureTheory.VectorMeasure X F} {B : E →L[ℝ] F →L[ℝ] G} {f : X → E},
  ¬CompleteSpace G → ∫ᵛ (x : X), f x ∂[B; μ] = 0
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv
HasDerivAt.arctan : ∀ {f : ℝ → ℝ} {f' x : ℝ}, HasDerivAt f f' x → HasDerivAt (fun x => Real.arctan (f x)) (1 / (1 + f x ^ 2) * f') x
-- Lean.DocString.Syntax
Lean.Doc.Syntax.arg_str : Lean.ParserDescr
-- Mathlib.Data.Multiset.Replicate
/-- `replicate n a` is the multiset containing only `a` with multiplicity `n`.  -/
Multiset.replicate : {α : Type u_1} → ℕ → α → Multiset α
-- Mathlib.Algebra.Algebra.Epi
/-- A commutative `R`-algebra `A` is epi, if the multiplication map `A ⊗[R] A → A` is injective.  -/
Algebra.IsEpi : (R : Type u_1) → (A : Type u_2) → [inst : CommSemiring R] → [inst_1 : Semiring A] → [Algebra R A] → Prop
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.Hom.commGroup.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] {G X : C}
  [inst_2 : CategoryTheory.GrpObj G] [inst_3 : CategoryTheory.BraidedCategory C]
  [inst_4 : CategoryTheory.IsCommMonObj G],
  CategoryTheory.Hom.commGroup = { toGroup := CategoryTheory.Hom.group, mul_comm := ⋯ }
-- Mathlib.Data.Multiset.Bind
Multiset.add_sigma : ∀ {α : Type u_1} {σ : α → Type u_4} (s t : Multiset α) (u : (a : α) → Multiset (σ a)),
  (s + t).sigma u = s.sigma u + t.sigma u
-- Mathlib.Analysis.Calculus.TangentCone.Basic
Filter.HasBasis.tangentConeAt_eq_biInter_closure : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : AddCommGroup E] [inst_1 : SMul 𝕜 E] [inst_2 : TopologicalSpace E] {s : Set E}
  {x : E} {ι : Sort u_3} {p : ι → Prop} {U : ι → Set E},
  (nhds 0).HasBasis p U →
    tangentConeAt 𝕜 s x = ⋂ i, ⋂ (_ : p i), closure (Set.univ • (U i ∩ (fun x_2 => x + x_2) ⁻¹' s))
-- Mathlib.Topology.Category.Sequential
Sequential.mk.inj : ∀ {toTop : TopCat} {is_sequential : SequentialSpace ↑toTop} {toTop_1 : TopCat}
  {is_sequential_1 : SequentialSpace ↑toTop_1},
  { toTop := toTop, is_sequential := is_sequential } = { toTop := toTop_1, is_sequential := is_sequential_1 } →
    toTop = toTop_1
-- Lean.Elab.Util
/-- safety: requires that `mkConst typeName _` and `γ` are definitionally equal  -/
Lean.Elab.mkElabAttribute : (γ : Type) →
  Lean.Name →
    Lean.Name →
      Lean.Name →
        Lean.Name → String → autoParam Lean.Name Lean.Elab.mkElabAttribute._auto_1 → IO (Lean.KeyedDeclsAttribute γ)
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.zero_lt_getElem!_toList_rco_iff : ∀ {m n i : ℕ}, 0 < (m...n).toList[i]! ↔ i < n - m ∧ 0 < i + m
-- Mathlib.Lean.Meta.Tactic.Rewrite
/-- Rewrites the type of `e` via some `eq`, then moves `e` into the new type via `Eq.mp`.

Rewrites with a fresh metavariable as the ambient goal.
Fails if the rewrite produces any subgoals.
 -/
Lean.Expr.rewriteType : Lean.Expr → Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
SSet.Subcomplex.Pairing.RankFunction.Cell.map.congr_simp : ∀ {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [inst : LinearOrder ι] {f : P.RankFunction ι} {i : ι}
  (c : f.Cell i) [inst_1 : P.IsProper], c.map = c.map
-- Std.Data.DTreeMap.Basic
/-- Returns the key-value pair with the `n`-th smallest key.  -/
Std.DTreeMap.entryAtIdx : {α : Type u} →
  {β : α → Type v} → {cmp : α → α → Ordering} → (t : Std.DTreeMap α β cmp) → (n : ℕ) → n < t.size → (a : α) × β a
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
/-- Adding a vector in the direction to a point produces a point in the subspace if and only if
the original point is in the subspace.  -/
AffineSubspace.vadd_mem_iff_mem_of_mem_direction : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {s : AffineSubspace k P} {v : V}, v ∈ s.direction → ∀ {p : P}, v +ᵥ p ∈ s ↔ p ∈ s
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cocone.instIsIsoExtendHom : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {s : CategoryTheory.Limits.Cocone F} {X : C} (f : s.pt ⟶ X) [CategoryTheory.IsIso f],
  CategoryTheory.IsIso (s.extendHom f)
-- Mathlib.RingTheory.Idempotents
CompleteOrthogonalIdempotents.pair_iffₛ : ∀ {R : Type u_4} [inst : CommSemiring R] {x y : R}, CompleteOrthogonalIdempotents ![x, y] ↔ x * y = 0 ∧ x + y = 1
-- Std.Data.DHashMap.Internal.Model
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.Raw₀.getKeyₘ : {α : Type u} →
  {β : α → Type v} →
    [inst : BEq α] → [inst_1 : Hashable α] → (m : Std.DHashMap.Internal.Raw₀ α β) → (a : α) → m.containsₘ a = true → α
-- Mathlib.Logic.Equiv.Prod
Equiv.Perm.prodExtendRight_apply_ne : ∀ {α₁ : Type u_9} {β₁ : Type u_10} [inst : DecidableEq α₁] (e : Equiv.Perm β₁) {a a' : α₁},
  a' ≠ a → ∀ (b : β₁), (Equiv.Perm.prodExtendRight a e) (a', b) = (a', b)
-- Mathlib.RepresentationTheory.Intertwining
Representation.IntertwiningMap.toFun_injective : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Semiring A] [inst_1 : Monoid G]
  [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid W] [inst_4 : Module A V] [inst_5 : Module A W]
  (ρ : Representation A G V) (σ : Representation A G W), Function.Injective fun f => f.toFun
-- Lean.Attributes
Lean.AttributeExtensionState.map : Lean.AttributeExtensionState → Std.HashMap Lean.Name Lean.AttributeImpl
-- Lean.Data.Trie
Lean.Data.Trie.brecOn_2.go : {α : Type} →
  {motive_1 : Lean.Data.Trie α → Sort u} →
    {motive_2 : Array (Lean.Data.Trie α) → Sort u} →
      {motive_3 : List (Lean.Data.Trie α) → Sort u} →
        (t : List (Lean.Data.Trie α)) →
          ((t : Lean.Data.Trie α) → t.below → motive_1 t) →
            ((t : Array (Lean.Data.Trie α)) → Lean.Data.Trie.below_1 t → motive_2 t) →
              ((t : List (Lean.Data.Trie α)) → Lean.Data.Trie.below_2 t → motive_3 t) →
                motive_3 t ×' Lean.Data.Trie.below_2 t
-- Mathlib.Order.WellFounded
StrictMono.le_apply : ∀ {β : Type u_2} [inst : LinearOrder β] [WellFoundedLT β] {f : β → β}, StrictMono f → ∀ {x : β}, x ≤ f x
-- Mathlib.Algebra.Ring.GrindInstances
CommRing.toGrindCommRing : (α : Type u_1) → [s : CommRing α] → Lean.Grind.CommRing α
-- Mathlib.Order.Hom.Bounded
BoundedOrderHom.mk.injEq : ∀ {α : Type u_6} {β : Type u_7} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : BoundedOrder α]
  [inst_3 : BoundedOrder β] (toOrderHom : α →o β) (map_top' : toOrderHom.toFun ⊤ = ⊤)
  (map_bot' : toOrderHom.toFun ⊥ = ⊥) (toOrderHom_1 : α →o β) (map_top'_1 : toOrderHom_1.toFun ⊤ = ⊤)
  (map_bot'_1 : toOrderHom_1.toFun ⊥ = ⊥),
  ({ toOrderHom := toOrderHom, map_top' := map_top', map_bot' := map_bot' } =
      { toOrderHom := toOrderHom_1, map_top' := map_top'_1, map_bot' := map_bot'_1 }) =
    (toOrderHom = toOrderHom_1)
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.RelCWComplex.disjoint_openCell_of_ne : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : Topology.RelCWComplex C D] {n m : ℕ}
  {i : Topology.RelCWComplex.cell C n} {j : Topology.RelCWComplex.cell C m},
  ⟨n, i⟩ ≠ ⟨m, j⟩ → Disjoint (Topology.RelCWComplex.openCell n i) (Topology.RelCWComplex.openCell m j)
-- Mathlib.GroupTheory.Perm.Cycle.Type
Equiv.Perm.IsThreeCycle.card_support : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {σ : Equiv.Perm α}, σ.IsThreeCycle → σ.support.card = 3
-- Mathlib.Algebra.Module.LocalizedModule.Submodule
Submodule.isLocalizedModule : ∀ {R : Type u_1} (S : Type u_2) {M : Type u_3} {N : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid N] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : Algebra R S] [inst_7 : Module S N] [inst_8 : IsScalarTower R S N] (p : Submonoid R)
  [inst_9 : IsLocalization p S] (f : M →ₗ[R] N) [inst_10 : IsLocalizedModule p f] (M' : Submodule R M),
  IsLocalizedModule p (Submodule.toLocalized' S p f M')
-- Qq.Match
Qq.Impl.«term_qq_match_:=_|_» : Lean.ParserDescr
-- Mathlib.Computability.TuringMachine.ToPartrec
_private.Mathlib.Computability.TuringMachine.ToPartrec.0.Turing.PartrecToTM2.splitAtPred.match_1.splitter : {α : Type u_1} →
  (motive : List α × Option α × List α → Sort u_2) →
    (x : List α × Option α × List α) → ((l₁ : List α) → (o : Option α) → (l₂ : List α) → motive (l₁, o, l₂)) → motive x
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.val_add : ∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [inst : CommRing A] [inst_1 : SetLike σ A]
  [inst_2 : AddSubgroupClass σ A] [inst_3 : AddCommMonoid ι] [inst_4 : DecidableEq ι] {𝒜 : ι → σ}
  [inst_5 : GradedRing 𝒜] {x : Submonoid A} (y1 y2 : HomogeneousLocalization 𝒜 x), (y1 + y2).val = y1.val + y2.val
-- Mathlib.Topology.Path
/-- Image of a path from `x` to `y` by a map which is continuous on the path.  -/
Path.map' : {X : Type u_1} →
  {Y : Type u_2} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] →
        {x y : X} → (γ : Path x y) → {f : X → Y} → ContinuousOn f (Set.range ⇑γ) → Path (f x) (f y)
-- Mathlib.Algebra.Lie.Abelian
LieModule.IsTrivial.mk : ∀ {L : Type v} {M : Type w} [inst : Bracket L M] [inst_1 : Zero M],
  (∀ (x : L) (m : M), ⁅x, m⁆ = 0) → LieModule.IsTrivial L M
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.lt_of_lt_of_eq : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α] {f g h : CauSeq α abs},
  f < g → g ≈ h → f < h