mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.ContMDiff.Defs
/-- `ContMDiffAt I I' n f x` indicates that the function `f : M → M'` between manifolds
is `n` times continuously differentiable at `x : M`.

`f` is `n` times continuously differentiable at `x` if it is continuous and it is `n` times
continuously differentiable around `x`, when read in the preferred chart at `x`.
The parameter `n` belongs to `ℕ∞ω` (accessible in the `ContDiff` scope), i.e. it can be a natural
number, `∞`, or `ω`, where `C^ω` corresponds to analytic functions.  -/
ContMDiffAt : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {H : Type u_3} →
            [inst_3 : TopologicalSpace H] →
              ModelWithCorners 𝕜 E H →
                {M : Type u_4} →
                  [inst_4 : TopologicalSpace M] →
                    [ChartedSpace H M] →
                      {E' : Type u_5} →
                        [inst_6 : NormedAddCommGroup E'] →
                          [inst_7 : NormedSpace 𝕜 E'] →
                            {H' : Type u_6} →
                              [inst_8 : TopologicalSpace H'] →
                                ModelWithCorners 𝕜 E' H' →
                                  {M' : Type u_7} →
                                    [inst : TopologicalSpace M'] →
                                      [ChartedSpace H' M'] → WithTop ℕ∞ → (M → M') → M → Prop
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.filter!.eq_2 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (f : (a : α) → β a → Bool) (size : ℕ) (k' : α) (v' : β k')
  (l' r' : Std.DTreeMap.Internal.Impl α β),
  Std.DTreeMap.Internal.Impl.filter! f (Std.DTreeMap.Internal.Impl.inner size k' v' l' r') =
    match f k' v' with
    | false => (Std.DTreeMap.Internal.Impl.filter! f l').link2! (Std.DTreeMap.Internal.Impl.filter! f r')
    | true =>
      Std.DTreeMap.Internal.Impl.link! k' v' (Std.DTreeMap.Internal.Impl.filter! f l')
        (Std.DTreeMap.Internal.Impl.filter! f r')
-- Mathlib.Topology.Algebra.Group.Basic
Filter.map_divRight_nhdsNE : ∀ {G : Type w} [inst : Group G] [inst_1 : TopologicalSpace G] [IsTopologicalGroup G] {c a : G},
  Filter.map (fun x => x / c) (nhdsWithin a {a}ᶜ) = nhdsWithin (a / c) {a / c}ᶜ
-- Mathlib.Algebra.Ring.BooleanRing
ofBoolAlg_inj : ∀ {α : Type u_1} {a b : AsBoolAlg α}, ofBoolAlg a = ofBoolAlg b ↔ a = b
-- Mathlib.Analysis.Complex.Angle
Complex.angle_one_right : ∀ {x : ℂ}, x ≠ 0 → InnerProductGeometry.angle x 1 = |x.arg|
-- Mathlib.Algebra.Order.Interval.Set.Instances
Set.Ioc.instPow : {R : Type u_1} → [inst : Semiring R] → [inst_1 : PartialOrder R] → [IsStrictOrderedRing R] → Pow ↑(Set.Ioc 0 1) ℕ
-- Mathlib.Algebra.Order.Group.Synonym
OrderDual.instInvolutiveInv : {α : Type u_1} → [InvolutiveInv α] → InvolutiveInv αᵒᵈ
-- Mathlib.Data.ENNReal.Inv
/-- See `ENNReal.div_div_cancel` for a simpler version assuming `a ≠ 0`, `a ≠ ∞`.  -/
ENNReal.div_div_cancel' : ∀ {a b : ENNReal}, (a = 0 → b = 0) → (a = ⊤ → b = 0) → a / (a / b) = b
-- Batteries.Lean.LawfulMonadLift
instLawfulMonadLiftTEIOExceptionCommandElabM_batteries : LawfulMonadLiftT (EIO Lean.Exception) Lean.Elab.Command.CommandElabM
-- Mathlib.Topology.Order.Bornology
Pi.instIsOrderBornology : ∀ {ι : Type u_2} {α : ι → Type u_3} [inst : (i : ι) → Preorder (α i)] [inst_1 : (i : ι) → Bornology (α i)]
  [∀ (i : ι), IsOrderBornology (α i)], IsOrderBornology ((i : ι) → α i)
-- Mathlib.Data.List.ToFinsupp
List.toFinsupp_concat_eq_toFinsupp_add_single : ∀ {R : Type u_2} [inst : AddZeroClass R] (x : R) (xs : List R)
  [inst_1 : DecidablePred fun i => (xs ++ [x]).getD i 0 ≠ 0] [inst_2 : DecidablePred fun i => xs.getD i 0 ≠ 0],
  (xs ++ [x]).toFinsupp = xs.toFinsupp + fun₀ | xs.length => x
-- Lean.Elab.PreDefinition.TerminationHint
Lean.Elab.instInhabitedPartialFixpointType : Inhabited Lean.Elab.PartialFixpointType
-- Mathlib.Algebra.Group.Equiv.Defs
AddEquiv.toEquiv_eq_coe : ∀ {M : Type u_4} {N : Type u_5} [inst : Add M] [inst_1 : Add N] (f : M ≃+ N), f.toEquiv = ↑f
-- Mathlib.Analysis.Convex.Independent
/-- If a family is convex independent, a point in the family is in the convex hull of some of the
points given by a subset of the index type if and only if the point's index is in this subset.  -/
ConvexIndependent.mem_convexHull_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] {p : ι → E},
  ConvexIndependent 𝕜 p → ∀ (s : Set ι) (i : ι), p i ∈ (convexHull 𝕜) (p '' s) ↔ i ∈ s
-- Mathlib.GroupTheory.FreeAbelianGroup
FreeAbelianGroup.sub_seq : ∀ {α β : Type u} (f g : FreeAbelianGroup (α → β)) (x : FreeAbelianGroup α), f - g <*> x = (f <*> x) - (g <*> x)
-- Mathlib.Tactic.Explode.Datatypes
Mathlib.Explode.Entries.mk.inj : ∀ {s : Lean.ExprMap Mathlib.Explode.Entry} {l : List Mathlib.Explode.Entry} {s_1 : Lean.ExprMap Mathlib.Explode.Entry}
  {l_1 : List Mathlib.Explode.Entry}, { s := s, l := l } = { s := s_1, l := l_1 } → s = s_1 ∧ l = l_1
-- Mathlib.Lean.Meta.RefinedDiscrTree.Initialize
/-- Information generated from imported modules.  -/
_private.Mathlib.Lean.Meta.RefinedDiscrTree.Initialize.0.Lean.Meta.RefinedDiscrTree.ImportErrorData : Type
-- Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero
Localization.liftOn_zero : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] {S : Submonoid M} {p : Type u_4} (f : M → ↥S → p)
  (H : ∀ {a c : M} {b d : ↥S}, (Localization.r S) (a, b) (c, d) → f a b = f c d), Localization.liftOn 0 f H = f 0 1
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.minKey?_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp],
  t₁.Equiv t₂ → t₁.minKey? = t₂.minKey?
-- Init.Data.Iterators.PostconditionMonad
Std.Iterators.instMonadLiftPostconditionT : {m : Type w → Type w'} →
  {n : Type w → Type w''} →
    [MonadLift m n] → MonadLift (Std.Iterators.PostconditionT m) (Std.Iterators.PostconditionT n)
-- Mathlib.Topology.Separation.Basic
/-- Let `x` be a point in a discrete subset `s` of a topological space, then there exists an open
set that only meets `s` at `x`.  -/
isOpen_inter_eq_singleton_of_mem_discrete : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X}, IsDiscrete s → ∀ {x : X}, x ∈ s → ∃ U, IsOpen U ∧ U ∩ s = {x}
-- Mathlib.Data.PFun
/-- A recursion principle for `PFun.fix`.  -/
PFun.fixInduction : {α : Type u_1} →
  {β : Type u_2} →
    {C : α → Sort u_7} →
      {f : α →. β ⊕ α} →
        {b : β} →
          {a : α} → b ∈ f.fix a → ((a' : α) → b ∈ f.fix a' → ((a'' : α) → Sum.inr a'' ∈ f a' → C a'') → C a') → C a
-- Lean.Server.CodeActions.Basic
Lean.Server.instInhabitedCodeActionProvider : Inhabited Lean.Server.CodeActionProvider
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
/-- The counit isomorphism of the equivalence
`widePullbackShapeOpEquiv : (WidePullbackShape J)ᵒᵖ ≌ WidePushoutShape J`  -/
CategoryTheory.Limits.widePushoutShapeUnopOp : (J : Type w) →
  (CategoryTheory.Limits.widePushoutShapeOp J).comp (CategoryTheory.Limits.widePullbackShapeUnop J) ≅
    CategoryTheory.Functor.id (CategoryTheory.Limits.WidePushoutShape J)
-- Mathlib.Analysis.Calculus.FDeriv.Congr
Filter.EventuallyEq.hasFDerivAt_iff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f₀ f₁ : E → F} {f' : E →L[𝕜] F} {x : E},
  f₀ =ᶠ[nhds x] f₁ → (HasFDerivAt f₀ f' x ↔ HasFDerivAt f₁ f' x)
-- Aesop.Search.Queue
Aesop.FIFOQueue.mk : Array Aesop.GoalRef → ℕ → Aesop.FIFOQueue
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.getEntryₘ_eq_getEntry : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : PartialEquivBEq α] [inst_2 : Hashable α]
  [inst_3 : LawfulHashable α] {m : Std.DHashMap.Internal.Raw₀ α β} (hm : Std.DHashMap.Internal.Raw.WFImp ↑m) {a : α}
  {h : m.containsₘ a = true},
  m.getEntryₘ a h = Std.Internal.List.getEntry a (Std.DHashMap.Internal.toListModel (↑m).buckets) ⋯
-- Mathlib.Algebra.Group.Submonoid.Operations
/-- An `AddEquiv` `φ` between two additive monoids `M` and `N` induces an `AddEquiv`
between a submonoid `S ≤ M` and the submonoid `φ(S) ≤ N`. See
`AddMonoidHom.addSubmonoidMap` for a variant for `AddMonoidHom`s.  -/
AddEquiv.addSubmonoidMap : {M : Type u_1} →
  {N : Type u_2} →
    [inst : AddZeroClass M] →
      [inst_1 : AddZeroClass N] → (e : M ≃+ N) → (S : AddSubmonoid M) → ↥S ≃+ ↥(AddSubmonoid.map e S)
-- Mathlib.Algebra.ContinuedFractions.Translations
GenContFract.partNums.eq_1 : ∀ {α : Type u_1} (g : GenContFract α), g.partNums = Stream'.Seq.map GenContFract.Pair.a g.s
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Over.comp_left : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X : T} (a b c : CategoryTheory.Over X) (f : a ⟶ b)
  (g : b ⟶ c),
  CategoryTheory.Over.Hom.left (CategoryTheory.CategoryStruct.comp f g) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left f) (CategoryTheory.Over.Hom.left g)
-- Mathlib.CategoryTheory.Monad.Limits
/-- (Impl) Prove that the lifted cone is limiting.  -/
CategoryTheory.Monad.ForgetCreatesLimits.liftedConeIsLimit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {T : CategoryTheory.Monad C} →
      {J : Type u} →
        [inst_1 : CategoryTheory.Category.{v, u} J] →
          (D : CategoryTheory.Functor J T.Algebra) →
            (c : CategoryTheory.Limits.Cone (D.comp T.forget)) →
              (t : CategoryTheory.Limits.IsLimit c) →
                CategoryTheory.Limits.IsLimit (CategoryTheory.Monad.ForgetCreatesLimits.liftedCone D c t)
-- Mathlib.Algebra.Lie.Extension
/-- An equivalence between the direct product and the corresponding one-field structure. This is
used to transfer the additive and scalar-multiple structure on the direct product to the type
synonym.  -/
LieAlgebra.ofProd : {R : Type u_1} →
  {L : Type u_3} →
    {M : Type u_4} →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [inst_2 : LieAlgebra R L] →
            [inst_3 : AddCommGroup M] →
              [inst_4 : Module R M] →
                [inst_5 : LieRingModule L M] →
                  [inst_6 : LieModule R L M] →
                    (c : ↥(LieModule.Cohomology.twoCocycle R L M)) → L × M ≃ LieAlgebra.ofTwoCocycle c
-- Mathlib.Algebra.Group.ULift
ULift.addCancelCommMonoid : {α : Type u} → [AddCancelCommMonoid α] → AddCancelCommMonoid (ULift.{u_1, u} α)
-- Mathlib.Algebra.Category.ModuleCat.Sheaf
SheafOfModules.sectionsFunctor_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  (R : CategoryTheory.Sheaf J RingCat) (M : SheafOfModules R), (SheafOfModules.sectionsFunctor R).obj M = M.sections
-- Mathlib.Analysis.Normed.Group.Seminorm
AddGroupNorm.toAddGroupSeminorm_eq_coe : ∀ {E : Type u_3} [inst : AddGroup E] {p : AddGroupNorm E}, ⇑p.toAddGroupSeminorm = ⇑p
-- Mathlib.Topology.EMetricSpace.Basic
lebesgue_number_lemma_of_emetric_nhds' : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {s : Set α} {c : (x : α) → x ∈ s → Set α},
  IsCompact s → (∀ (x : α) (hx : x ∈ s), c x hx ∈ nhds x) → ∃ δ > 0, ∀ x ∈ s, ∃ y, Metric.eball x δ ⊆ c ↑y ⋯
-- Mathlib.Combinatorics.SetFamily.Shatter
Finset.shatterer_idem : ∀ {α : Type u_1} [inst : DecidableEq α] {𝒜 : Finset (Finset α)}, 𝒜.shatterer.shatterer = 𝒜.shatterer
-- Mathlib.Algebra.Group.Pointwise.Set.Card
Cardinal.mk_smul_set : ∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] (a : G) (s : Set α),
  Cardinal.mk ↑(a • s) = Cardinal.mk ↑s
-- Mathlib.Algebra.Ring.BooleanRing
Bool.zero_eq_false : 0 = false
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.toList_emptyWithCapacity : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {c : ℕ} {β : Type v},
  Std.DHashMap.Const.toList (Std.DHashMap.emptyWithCapacity c) = []
-- Mathlib.Data.DFinsupp.Notation
/-- Display `DFinsupp` using `fun₀` notation.  -/
DFinsupp.instRepr : {α : Type u_1} →
  {β : α → Type u_2} → [Repr α] → [(i : α) → Repr (β i)] → [inst : (i : α) → Zero (β i)] → Repr (Π₀ (a : α), β a)
-- Mathlib.Analysis.Convex.Deriv
StrictConcaveOn.deriv_lt_slope : ∀ {S : Set ℝ} {f : ℝ → ℝ} {x y : ℝ},
  StrictConcaveOn ℝ S f → x ∈ S → y ∈ S → x < y → DifferentiableAt ℝ f y → deriv f y < slope f x y
-- Mathlib.Order.Filter.Finite
/-- A special case of `iInf_principal` that is safe to mark `simp`.  -/
Filter.iInf_principal' : ∀ {α : Type u} {ι : Type w} [Finite ι] (f : ι → Set α), ⨅ i, Filter.principal (f i) = Filter.principal (⋂ i, f i)
-- Lean.Meta.Sym.DSimp.DSimpM
Lean.Meta.Sym.DSimp.getMethods : Lean.Meta.Sym.DSimp.DSimpM Lean.Meta.Sym.DSimp.Methods
-- Std.Sat.AIG.Lemmas
Std.Sat.AIG.Ref.gate_cast : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {aig1 aig2 : Std.Sat.AIG α} (ref : aig1.Ref)
  (h : aig1.decls.size ≤ aig2.decls.size), (ref.cast h).gate = ref.gate
-- Mathlib.Data.Set.Finite.Basic
/-- **Alias** of `Set.Finite.sdiff`. -/
Set.Finite.diff : ∀ {α : Type u} {s t : Set α}, s.Finite → (s \ t).Finite
-- Std.Data.HashSet.Lemmas
Std.HashSet.isEmpty_union : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashSet α} [EquivBEq α] [LawfulHashable α],
  (m₁ ∪ m₂).isEmpty = (m₁.isEmpty && m₂.isEmpty)
-- Mathlib.Analysis.LocallyConvex.Polar
/-- Given a subset `s` in a monoid `M` (over a commutative ring `R`), the polar `polar R s` is the
subset of `StrongDual R M` consisting of those functionals which evaluate to something of norm at
most one at all points `z ∈ s`.  -/
StrongDual.polar : (R : Type u_4) →
  [inst : NormedCommRing R] →
    {M : Type u_5} →
      [inst_1 : AddCommMonoid M] → [inst_2 : TopologicalSpace M] → [inst_3 : Module R M] → Set M → Set (StrongDual R M)
-- Init.Data.List.Sublist
List.map_subset : ∀ {α : Type u_1} {β : Type u_2} {l₁ l₂ : List α} (f : α → β), l₁ ⊆ l₂ → List.map f l₁ ⊆ List.map f l₂
-- Mathlib.Algebra.Category.MonCat.FilteredColimits
/-- Given a cocone `t` of `F`, the induced additive monoid homomorphism from the colimit
to the cocone point. As a function, this is simply given by the induced map of the
corresponding cocone in `Type`. The only thing left to see is that it is an additive monoid
homomorphism.  -/
AddMonCat.FilteredColimits.colimitDesc : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    (F : CategoryTheory.Functor J AddMonCat) →
      [inst_1 : CategoryTheory.IsFiltered J] →
        (t : CategoryTheory.Limits.Cocone F) → AddMonCat.FilteredColimits.colimit F ⟶ t.pt
-- Mathlib.Order.Lattice
Lattice.toSemilatticeInf : {α : Type u} → [self : Lattice α] → SemilatticeInf α
-- Aesop.Builder.Basic
Aesop.RuleBuilderOptions.default : Aesop.RuleBuilderOptions
-- Mathlib.Topology.Instances.ENNReal.Lemmas
/-- **Alias** of `Metric.isClosed_closedEBall`. -/
EMetric.isClosed_closedBall : ∀ {α : Type u_1} [inst : PseudoEMetricSpace α] {a : α} {r : ENNReal}, IsClosed (Metric.closedEBall a r)
-- Lean.Parser.Basic
Lean.Parser.rawIdentNoAntiquot : Lean.Parser.Parser
-- Mathlib.Order.Hom.Basic
OrderHom.mk.injEq : ∀ {α : Type u_6} {β : Type u_7} [inst : Preorder α] [inst_1 : Preorder β] (toFun : α → β) (monotone' : Monotone toFun)
  (toFun_1 : α → β) (monotone'_1 : Monotone toFun_1),
  ({ toFun := toFun, monotone' := monotone' } = { toFun := toFun_1, monotone' := monotone'_1 }) = (toFun = toFun_1)
-- Mathlib.Order.Birkhoff
OrderIso.infIrredUpperSet_symm_apply : ∀ {α : Type u_1} [inst : SemilatticeInf α] [inst_1 : OrderTop α] [inst_2 : Finite α] (s : { s // InfIrred s })
  [inst_3 : Fintype ↥↑s], OrderIso.infIrredUpperSet.symm s = (↑↑s).toFinset.inf id
-- Mathlib.Topology.Compactness.Paracompact
Topology.IsClosedEmbedding.paracompactSpace : ∀ {X : Type v} {Y : Type w} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [ParacompactSpace Y] {e : X → Y},
  Topology.IsClosedEmbedding e → ParacompactSpace X
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
/-- Eta-expanded form of `MeasureTheory.StronglyMeasurable.const_nsmul` -/
MeasureTheory.StronglyMeasurable.fun_const_nsmul : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {mα : MeasurableSpace α} [inst : TopologicalSpace β] [inst_1 : AddMonoid β]
  [ContinuousAdd β], MeasureTheory.StronglyMeasurable f → ∀ (n : ℕ), MeasureTheory.StronglyMeasurable fun i => n • f i
-- Mathlib.LinearAlgebra.Span.Basic
LinearMap.toSpanSingleton_smul : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {S : Type u_8}
  [inst_3 : Monoid S] [inst_4 : DistribMulAction S M] [inst_5 : SMulCommClass R S M] (r : S) (x : M),
  LinearMap.toSpanSingleton R M (r • x) = r • LinearMap.toSpanSingleton R M x
-- Mathlib.Analysis.Calculus.LineDeriv.Basic
lineDifferentiableWithinAt_congr_set : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {E : Type u_3} [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace 𝕜 E] {f : E → F}
  {s t : Set E} {x v : E},
  s =ᶠ[nhds x] t → (LineDifferentiableWithinAt 𝕜 f s x v ↔ LineDifferentiableWithinAt 𝕜 f t x v)
-- Mathlib.Combinatorics.Enumerative.DoubleCounting
Finset.sum_sum_bipartiteAbove_eq_sum_sum_bipartiteBelow : ∀ {R : Type u_1} {α : Type u_2} {β : Type u_3} (r : α → β → Prop) {s : Finset α} {t : Finset β} [inst : AddCommMonoid R]
  (f : α → β → R) [inst_1 : (a : α) → (b : β) → Decidable (r a b)],
  ∑ a ∈ s, ∑ b ∈ Finset.bipartiteAbove r t a, f a b = ∑ b ∈ t, ∑ a ∈ Finset.bipartiteBelow r s b, f a b
-- Lean.ScopedEnvExtension
Lean.ScopedEnvExtension.Entry.scoped.injEq : ∀ {α : Type} (a : Lean.Name) (a_1 : α) (a_2 : Lean.Name) (a_3 : α),
  (Lean.ScopedEnvExtension.Entry.scoped a a_1 = Lean.ScopedEnvExtension.Entry.scoped a_2 a_3) = (a = a_2 ∧ a_1 = a_3)
-- Mathlib.Algebra.Category.Grp.Basic
AddGrpCat.instCategory : CategoryTheory.Category.{u, u + 1} AddGrpCat
-- Mathlib.GroupTheory.Congruence.Basic
Con.comap_conGen_equiv : ∀ {M : Type u_4} {N : Type u_5} [inst : Mul M] [inst_1 : Mul N] (f : M ≃* N) (rel : N → N → Prop),
  Con.comap ⇑f ⋯ (conGen rel) = conGen fun x y => rel (f x) (f y)
-- Mathlib.Order.Preorder.Chain
Flag.mem_coe_iff : ∀ {α : Type u_1} [inst : LE α] {s : Flag α} {a : α}, a ∈ ↑s ↔ a ∈ s
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.mem_of_mem_map : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α] {f : α → β → γ} {k : α}, m.WF → k ∈ Std.HashMap.Raw.map f m → k ∈ m
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.blsub_type : ∀ {α : Type u} (r : α → α → Prop) [inst : IsWellOrder α r]
  (f : (a : Ordinal.{u}) → a < Ordinal.type r → Ordinal.{max u v}),
  (Ordinal.type r).blsub f = Ordinal.lsub fun a => f ((Ordinal.typein r).toRelEmbedding a) ⋯
-- Mathlib.Lean.MessageData.ForExprs
/-- The `MessageData` whose expressions will be iterated over.  -/
Lean.MessageData.Exprs.msg : Lean.MessageData.Exprs → Lean.MessageData
-- Mathlib.Topology.UniformSpace.UniformConvergence
UniformCauchySeqOn.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : UniformSpace β] (F : ι → α → β) (p : Filter ι) (s : Set α),
  UniformCauchySeqOn F p s = ∀ u ∈ uniformity β, ∀ᶠ (m : ι × ι) in p ×ˢ p, ∀ x ∈ s, (F m.1 x, F m.2 x) ∈ u
-- Std.Tactic.BVDecide.Normalize.BitVec
Std.Tactic.BVDecide.Normalize.BitVec.const_beq_add_const_beq : ∀ {w c : ℕ} {a : BitVec w} {b : ℕ},
  (BitVec.ofNat w c == a + BitVec.ofNat w b) = (a == BitVec.ofNat w c - BitVec.ofNat w b)
-- Mathlib.CategoryTheory.MorphismProperty.LiftingProperty
CategoryTheory.MorphismProperty.llp_isMultiplicative : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (T : CategoryTheory.MorphismProperty C), T.llp.IsMultiplicative
-- Lean.Elab.Arg
Lean.Elab.Term.Arg.stx.sizeOf_spec : ∀ (val : Lean.Syntax), sizeOf (Lean.Elab.Term.Arg.stx val) = 1 + sizeOf val
-- Init.Data.SInt.Lemmas
Int8.ofIntLE_int32ToInt : ∀ (x : Int32) {h₁ : Int8.minValue.toInt ≤ x.toInt} {h₂ : x.toInt ≤ Int8.maxValue.toInt},
  Int8.ofIntLE x.toInt h₁ h₂ = x.toInt8
-- Mathlib.Order.Comparable
/-- A partial order where any two elements are comparable is a linear order.  -/
Relation.linearOrderOfSymmGen : {α : Type u_1} →
  [inst : PartialOrder α] →
    [decLE : DecidableLE α] →
      [decLT : DecidableLT α] →
        [decEq : DecidableEq α] → (∀ (a b : α), Relation.SymmGen (fun x1 x2 => x1 ≤ x2) a b) → LinearOrder α
-- Mathlib.Data.Finsupp.ToDFinsupp
/-- `Finsupp.split` is an additive equivalence between `(Σ i, η i) →₀ N` and `Π₀ i, (η i →₀ N)`.  -/
sigmaFinsuppAddEquivDFinsupp : {ι : Type u_1} →
  {η : ι → Type u_4} → {N : Type u_5} → [inst : AddZeroClass N] → ((i : ι) × η i →₀ N) ≃+ Π₀ (i : ι), η i →₀ N
-- Init.Data.Array.Zip
Array.zipWithM_eq_mapM_id_zipWith : ∀ {α : Type u_1} {β : Type u_2} {γ : Type v} {m : Type v → Type w} [inst : Monad m] [LawfulMonad m] {f : α → β → m γ}
  {as : Array α} {bs : Array β}, Array.zipWithM f as bs = Array.mapM id (Array.zipWith f as bs)
-- Lean.Message
Lean.MessageLog.instAppend : Append Lean.MessageLog
-- Mathlib.Algebra.Module.SpanRank
Submodule.spanFinrank_subsingleton : ∀ {R : Type u_1} {M : Type u} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Subsingleton R]
  (p : Submodule R M), p.spanFinrank = 0
-- Mathlib.MeasureTheory.MeasurableSpace.Basic
/-- **Alias** of the reverse direction of `measurable_iff_le_map`. -/
Measurable.of_le_map : ∀ {α : Type u_1} {β : Type u_2} {m₁ : MeasurableSpace α} {m₂ : MeasurableSpace β} {f : α → β},
  m₂ ≤ MeasurableSpace.map f m₁ → Measurable f
-- Mathlib.AlgebraicTopology.SimplicialSet.NonsingularColimit
/-- If `X` is a nonsingular simplicial set, `X` is the colimit of `Δ[x.dim]`
for all nondegenerate simplices `x : X.N`.  -/
SSet.isColimitCoconeN' : (X : SSet) → [inst : X.Nonsingular] → CategoryTheory.Limits.IsColimit X.coconeN'
-- Std.Http.Data.URI.Encoding
/-- Creates an `EncodedString` from a `String`, panicking if the string is not a valid percent-encoded string.
 -/
Std.Http.URI.EncodedString.ofString! : {r : UInt8 → Bool} → String → Std.Http.URI.EncodedString r
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.IsAffineOpen.isoSpec_hom_fromSpec_assoc : ∀ {X : AlgebraicGeometry.Scheme} {U : X.Opens} (hU : AlgebraicGeometry.IsAffineOpen U) {Z : AlgebraicGeometry.Scheme}
  (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp hU.isoSpec.hom (CategoryTheory.CategoryStruct.comp hU.fromSpec h) =
    CategoryTheory.CategoryStruct.comp U.ι h
-- Mathlib.Topology.Category.LightProfinite.Sequence
LightProfinite.instCoeNatCarrierToTopAndTotallyDisconnectedSpaceSecondCountableTopologyNatUnionInfty : Coe ℕ ↑LightProfinite.NatUnionInfty.toTop
-- Std.Data.Internal.Cut
Std.Internal.IsStrictCut.eq : ∀ {α : Type u} {cmp : α → α → Ordering} {cut : α → Ordering} [self : Std.Internal.IsStrictCut cmp cut] (k : α) {k' : α},
  cut k' = Ordering.eq → cut k = cmp k' k
-- Lean.Elab.PreDefinition.PartialFixpoint.Eqns
Lean.Elab.PartialFixpoint.EqnInfo.mk.inj : ∀ {declName : Lean.Name} {levelParams : List Lean.Name} {type value : Lean.Expr} {declNames : Array Lean.Name}
  {declNameNonRec : Lean.Name} {fixedParamPerms : Lean.Elab.FixedParamPerms}
  {fixpointType : Array Lean.Elab.PartialFixpointType} {declName_1 : Lean.Name} {levelParams_1 : List Lean.Name}
  {type_1 value_1 : Lean.Expr} {declNames_1 : Array Lean.Name} {declNameNonRec_1 : Lean.Name}
  {fixedParamPerms_1 : Lean.Elab.FixedParamPerms} {fixpointType_1 : Array Lean.Elab.PartialFixpointType},
  { declName := declName, levelParams := levelParams, type := type, value := value, declNames := declNames,
        declNameNonRec := declNameNonRec, fixedParamPerms := fixedParamPerms, fixpointType := fixpointType } =
      { declName := declName_1, levelParams := levelParams_1, type := type_1, value := value_1,
        declNames := declNames_1, declNameNonRec := declNameNonRec_1, fixedParamPerms := fixedParamPerms_1,
        fixpointType := fixpointType_1 } →
    declName = declName_1 ∧
      levelParams = levelParams_1 ∧
        type = type_1 ∧
          value = value_1 ∧
            declNames = declNames_1 ∧
              declNameNonRec = declNameNonRec_1 ∧ fixedParamPerms = fixedParamPerms_1 ∧ fixpointType = fixpointType_1
-- LeanSearchClient.LoogleSyntax
LeanSearchClient.LoogleResult.failure : String → Option (List String) → LeanSearchClient.LoogleResult