mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
SSet.Truncated.StrictSegal.spineToSimplex_vertex : ∀ {n : ℕ} {X : SSet.Truncated (n + 1)} (sx : X.StrictSegal) (m : ℕ) (h : m ≤ n + 1) (i : Fin (m + 1)) (f : X.Path m),
  (CategoryTheory.ConcreteCategory.hom
        (X.map (SimplexCategory.Truncated.Hom.tr ({ len := 0 }.const { len := m } i) ⋯ h).op))
      (sx.spineToSimplex m h f) =
    f.vertex i
-- Init.Data.List.ToArray
/-- Unapplied variant of `push_toArray`, useful for monadic reasoning.  -/
List.push_toArray_fun : ∀ {α : Type u_1} (l : List α), l.toArray.push = fun a => (l ++ [a]).toArray
-- Mathlib.Data.PFunctor.Univariate.M
/-- given a tree generated by `F`, `head` gives us the first piece of data
it contains  -/
PFunctor.M.head : {F : PFunctor.{uA, uB}} → F.M → F.A
-- Init.Data.BitVec.Bootstrap
BitVec.toNat_cons : ∀ {w : ℕ} (b : Bool) (x : BitVec w), (BitVec.cons b x).toNat = b.toNat <<< w ||| x.toNat
-- Mathlib.Order.Filter.Map
Filter.NeBot.comap_of_image_mem : ∀ {α : Type u_1} {β : Type u_2} {f : Filter β} {m : α → β},
  f.NeBot → ∀ {s : Set α}, m '' s ∈ f → (Filter.comap m f).NeBot
-- Std.Data.Iterators.Combinators.Monadic.Zip
/-- Internal state of the `zip` combinator. Do not depend on its internals.
 -/
Std.Iterators.Types.Zip : (α₁ : Type w) → (m : Type w → Type w') → {β₁ : Type w} → [Std.Iterator α₁ m β₁] → Type w → Type w → Type w
-- Mathlib.Topology.FiberBundle.Basic
FiberBundleCore.localTrivAsPartialEquiv_symm : ∀ {ι : Type u_1} {B : Type u_2} {F : Type u_3} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
  (Z : FiberBundleCore ι B F) (i : ι), (Z.localTrivAsPartialEquiv i).symm = (Z.localTriv i).symm
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getD_union : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {k : α} {fallback : β k}, (t₁ ∪ t₂).getD k fallback = t₂.getD k (t₁.getD k fallback)
-- Mathlib.MeasureTheory.Group.FoelnerFilter
IsAddFoelner.mean_vadd_eq_mean : ∀ {G : Type u_1} {X : Type u_2} [inst : MeasurableSpace X] {μ : MeasureTheory.Measure X} [inst_1 : AddGroup G]
  [inst_2 : AddAction G X] {ι : Type u_3} {u : Ultrafilter ι} {F : ι → Set X}
  [MeasureTheory.VAddInvariantMeasure G X μ],
  IsAddFoelner G μ (↑u) F → ∀ (g : G) (s : Set X), IsAddFoelner.mean μ u F (g +ᵥ s) = IsAddFoelner.mean μ u F s
-- Mathlib.RingTheory.Localization.AtPrime.Basic
Ideal.IsMaximal.of_isLocalization_of_disjoint : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) {S : Type u_4} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [IsLocalization M S] {J : Ideal S} [(Ideal.under R J).IsMaximal], J.IsMaximal
-- Mathlib.Computability.EpsilonNFA
εNFA.isPath_nil : ∀ {α : Type u} {σ : Type v} (M : εNFA α σ) {s t : σ}, M.IsPath s t [] ↔ s = t
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.leftUnitor_hom_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X : CategoryTheory.AddMon C),
  (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom.hom =
    (CategoryTheory.MonoidalCategoryStruct.leftUnitor X.X).hom
-- Mathlib.Algebra.Ring.Hom.Defs
RingHom.cancel_left : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β}
  {x_2 : NonAssocSemiring γ} {g : β →+* γ} {f₁ f₂ : α →+* β}, Function.Injective ⇑g → (g.comp f₁ = g.comp f₂ ↔ f₁ = f₂)
-- Mathlib.Tactic.DepRewrite
/-- Cleanup casts introduced by `rewrite!` in `e`.
The result is expected to be defeq to the original expression.  -/
Mathlib.Tactic.DepRewrite.cleanupCasts : Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Algebra.Polynomial.Laurent
/-- This is a version of `exists_T_pow` stated as an induction principle.  -/
LaurentPolynomial.induction_on_mul_T : ∀ {R : Type u_1} [inst : Semiring R] {motive : LaurentPolynomial R → Prop} (f : LaurentPolynomial R),
  (∀ (f : Polynomial R) (n : ℕ), motive (Polynomial.toLaurent f * LaurentPolynomial.T (-↑n))) → motive f
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
/-- Linearization proof for `%`
- If `?y = some y`, then it is a proof for `a % b = y%k` where `c` is a proof that `b = k`
- If `?y = none`, then it is a proof for `a % b = a%k` where `c` is a proof that `b = k`. `a` is a numeral in this case.
 -/
Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.mod : ℤ → Option Int.Internal.Linear.Var → Lean.Meta.Grind.Arith.Cutsat.EqCnstr → Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof
-- Mathlib.LinearAlgebra.ExteriorAlgebra.Basis
/-- If `b` is a basis of `M` (indexed by a linearly ordered type), the basis of the exterior
algebra of `M` formed by the `n`-fold exterior products of elements of `b` for each `n`.  -/
Module.Basis.ExteriorAlgebra : {R : Type u_1} →
  {M : Type u_2} →
    {I : Type u_3} →
      [LinearOrder I] →
        [inst : CommRing R] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : Module R M] → Module.Basis I R M → Module.Basis (Finset I) R (ExteriorAlgebra R M)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.DocumentSymbolParams : Type
-- Mathlib.CategoryTheory.Distributive.Monoidal
CategoryTheory.coprod_inr_leftDistrib_hom_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Limits.HasBinaryCoproducts C] [inst_3 : CategoryTheory.IsMonoidalLeftDistrib C]
  {X Y Z Z_1 : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj X (Y ⨿ Z) ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.leftDistrib X Y Z).hom h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X CategoryTheory.Limits.coprod.inr) h
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
/-- `NonUnitalStarAlgHom` to `⊤ : NonUnitalStarSubalgebra R A`.  -/
NonUnitalStarAlgebra.toTop : {R : Type u} →
  {A : Type v} →
    [inst : CommSemiring R] →
      [inst_1 : StarRing R] →
        [inst_2 : NonUnitalSemiring A] →
          [inst_3 : StarRing A] →
            [inst_4 : Module R A] →
              [inst_5 : IsScalarTower R A A] → [inst_6 : SMulCommClass R A A] → [inst_7 : StarModule R A] → A →⋆ₙₐ[R] ↥⊤
-- Mathlib.CategoryTheory.Bicategory.Opposites
Bicategory.Opposite.homCategory : {B : Type u} → [inst : CategoryTheory.Bicategory B] → (a b : Bᵒᵖ) → CategoryTheory.Category.{w, v} (a ⟶ b)
-- Mathlib.SetTheory.Cardinal.ENat
/-- **Alias** of `Cardinal.toENat_eq_natCast`. -/
Cardinal.toENat_eq_nat : ∀ {c : Cardinal.{u}} {n : ℕ}, Cardinal.toENat c = ↑n ↔ c = ↑n
-- Mathlib.Combinatorics.SimpleGraph.Density
SimpleGraph.swap_mem_interedges_iff : ∀ {α : Type u_4} (G : SimpleGraph α) [inst : DecidableRel G.Adj] {s t : Finset α} {x : α × α},
  x.swap ∈ G.interedges s t ↔ x ∈ G.interedges t s
-- Std.Time.Internal.UnitVal
/-- Creates a `UnitVal` from a `Nat`.
 -/
Std.Time.Internal.UnitVal.ofNat : {α : ℚ} → ℕ → Std.Time.Internal.UnitVal α
-- Lean.Util.ParamMinimizer
Lean.Util.ParamMinimizer.instInhabitedStatus.default : Lean.Util.ParamMinimizer.Status
-- Mathlib.Topology.VectorBundle.Basic
VectorBundleCore.addCommGroupFiber : {R : Type u_1} →
  {B : Type u_2} →
    {F : Type u_3} →
      [inst : NontriviallyNormedField R] →
        [inst_1 : NormedAddCommGroup F] →
          [inst_2 : NormedSpace R F] →
            [inst_3 : TopologicalSpace B] →
              {ι : Type u_5} → (Z : VectorBundleCore R B F ι) → (x : B) → AddCommGroup (Z.Fiber x)
-- Mathlib.Algebra.Group.Hom.Instances
MonoidHom.compl₂.eq_1 : ∀ {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} [inst : MulOneClass M] [inst_1 : MulOneClass N]
  [inst_2 : CommMonoid P] [inst_3 : MulOneClass Q] (f : M →* N →* P) (g : Q →* N), f.compl₂ g = g.compHom'.comp f
-- Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
SimpleGraph.Walk.IsSubwalk.edges_isInfix : ∀ {V : Type u_1} {G : SimpleGraph V} {u v u' v' : V} {p₁ : G.Walk u v} {p₂ : G.Walk u' v'},
  p₁.IsSubwalk p₂ → p₁.edges <:+: p₂.edges
-- Mathlib.RingTheory.Polynomial.Resultant.Basic
/-- `Res(X + r, g) = g(-r)`  -/
Polynomial.resultant_X_add_C_left : ∀ {R : Type u_1} [inst : CommRing R] (g : Polynomial R) (n : ℕ) (r : R),
  g.natDegree ≤ n → (Polynomial.X + Polynomial.C r).resultant g 1 n = Polynomial.eval (-r) g
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.preimage_div_preimage_subset : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Group α] [inst_1 : DivisionMonoid β] [inst_2 : FunLike F α β]
  [MonoidHomClass F α β] (m : F) {s t : Set β}, ⇑m ⁻¹' s / ⇑m ⁻¹' t ⊆ ⇑m ⁻¹' (s / t)
-- Mathlib.Tactic.Linarith.Oracle.FourierMotzkin
Mathlib.Tactic.Linarith.instToFormatCompSource : Std.ToFormat Mathlib.Tactic.Linarith.CompSource
-- Mathlib.NumberTheory.Modular
/-- An auxiliary result en route to `ModularGroup.c_eq_zero` and `cases_of_mem_fd_smul_mem_fd`.  -/
ModularGroup.abs_c_le_one : ∀ {g : Matrix.SpecialLinearGroup (Fin 2) ℤ} {z : UpperHalfPlane},
  z ∈ ModularGroup.fd → g • z ∈ ModularGroup.fd → |↑g 1 0| ≤ 1
-- Mathlib.Algebra.Order.UpperLower
lowerClosure_zero : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : Preorder α], lowerClosure 0 = 0
-- Lean.Parser.Types
Lean.Parser.instInhabitedParserInfo : Inhabited Lean.Parser.ParserInfo
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.foldM_eq_foldlM_toArray : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) {δ : Type w} {m' : Type w → Type w'}
  [inst : Monad m'] [LawfulMonad m'] {f : δ → (a : α) → β a → m' δ} {init : δ},
  Std.DHashMap.Raw.foldM f init ↑m = Array.foldlM (fun a b => f a b.fst b.snd) init (↑m).toArray
-- Mathlib.Algebra.Homology.QuasiIso
HomologicalComplex.quasiIso.congr_simp : ∀ {ι : Type u_1} (C : Type u) [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] (c : ComplexShape ι)
  [inst_2 : CategoryTheory.CategoryWithHomology C] ⦃X Y : HomologicalComplex C c⦄ (x x_1 : X ⟶ Y),
  x = x_1 → HomologicalComplex.quasiIso C c x = HomologicalComplex.quasiIso C c x_1
-- Mathlib.Combinatorics.SimpleGraph.Acyclic
SimpleGraph.isTree_iff_connected_and_card : ∀ {V : Type u_1} {G : SimpleGraph V} [Finite V], G.IsTree ↔ G.Connected ∧ Nat.card ↑G.edgeSet + 1 = Nat.card V
-- Mathlib.Probability.Kernel.Category.SFinKer
/-- The morphisms in `SFinKer` from `X` to `Y` are the s-finite kernels from `X` to `Y`.  -/
SFinKer.Hom : SFinKer → SFinKer → Type u
-- Mathlib.RingTheory.TensorProduct.Quotient
Algebra.TensorProduct.quotIdealMapEquivQuotTensor_mk : ∀ {A : Type u_1} (B : Type u_2) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] (I : Ideal A) (b : B),
  (Algebra.TensorProduct.quotIdealMapEquivQuotTensor B I) ((Ideal.Quotient.mk (Ideal.map (algebraMap A B) I)) b) =
    1 ⊗ₜ[A] b
-- Mathlib.CategoryTheory.Sites.ConstantSheaf
CategoryTheory.constantPresheafAdj_unit_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (D : Type u_2)
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {T : C} (hT : CategoryTheory.Limits.IsTerminal T) (X : D),
  (CategoryTheory.constantPresheafAdj D hT).unit.app X = CategoryTheory.CategoryStruct.id X
-- Mathlib.Topology.TietzeExtension
/-- **Tietze extension theorem** for real-valued bounded continuous maps, a version for a closed
embedding and a bounded continuous function that takes values in a non-trivial closed interval.
See also `exists_extension_forall_mem_of_isClosedEmbedding` for a more general statement that works
for any interval (finite or infinite, open or closed).

If `e : X → Y` is a closed embedding and `f : X →ᵇ ℝ` is a bounded continuous function such that
`f x ∈ [a, b]` for all `x`, where `a ≤ b`, then there exists a bounded continuous function
`g : Y →ᵇ ℝ` such that `g y ∈ [a, b]` for all `y` and `g ∘ e = f`.  -/
BoundedContinuousFunction.exists_extension_forall_mem_Icc_of_isClosedEmbedding : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [NormalSpace Y]
  (f : BoundedContinuousFunction X ℝ) {a b : ℝ} {e : X → Y},
  (∀ (x : X), f x ∈ Set.Icc a b) →
    a ≤ b → Topology.IsClosedEmbedding e → ∃ g, (∀ (y : Y), g y ∈ Set.Icc a b) ∧ ⇑g ∘ e = ⇑f
-- Mathlib.FieldTheory.AlgebraicClosure
/-- An intermediate field of `E / F` is contained in the algebraic closure of `F` in `E`
if all of its elements are algebraic over `F`.  -/
le_algebraicClosure' : ∀ (F : Type u_1) (E : Type u_2) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {L : IntermediateField F E},
  (∀ (x : ↥L), IsAlgebraic F x) → L ≤ algebraicClosure F E
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.inv_hom_whiskerRight : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {f g : a ⟶ b} (η : f ≅ g) (h : b ⟶ c),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight η.inv h)
      (CategoryTheory.Bicategory.whiskerRight η.hom h) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.comp g h)
-- Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
CategoryTheory.ObjectProperty.ιOfLE_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P P' : CategoryTheory.ObjectProperty C} (h : P ≤ P')
  {X Y : P.FullSubcategory} (f : X ⟶ Y),
  (CategoryTheory.ObjectProperty.ιOfLE h).map f = CategoryTheory.ObjectProperty.homMk f.hom
-- Mathlib.Algebra.Homology.ShortComplex.Exact
/-- the condition that `s` is a section of `S.g`  -/
CategoryTheory.ShortComplex.Splitting.s_g : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S : CategoryTheory.ShortComplex C} (self : S.Splitting),
  CategoryTheory.CategoryStruct.comp self.s S.g = CategoryTheory.CategoryStruct.id S.X₃
-- Mathlib.CategoryTheory.Bicategory.LocallyGroupoid
CategoryTheory.Bicategory.Pith.rightUnitor_inv_iso_inv : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] {a b : CategoryTheory.Bicategory.Pith B} (x : a ⟶ b),
  (CategoryTheory.Bicategory.rightUnitor x).inv.iso.inv = (CategoryTheory.Bicategory.rightUnitor x.of).hom
-- Mathlib.Analysis.Calculus.FDeriv.Add
DifferentiableOn.sub : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f g : E → F}
  {s : Set E}, DifferentiableOn 𝕜 f s → DifferentiableOn 𝕜 g s → DifferentiableOn 𝕜 (f - g) s
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
/-- Every cokernel of `g ≫ f` is also a cokernel of `f`, as long as `f ≫ c.π` vanishes.  -/
CategoryTheory.Limits.isCokernelOfComp : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y : C} →
        {f : X ⟶ Y} →
          {W : C} →
            (g : W ⟶ X) →
              (h : W ⟶ Y) →
                {c : CategoryTheory.Limits.CokernelCofork h} →
                  CategoryTheory.Limits.IsColimit c →
                    (hf : CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.Cofork.π c) = 0) →
                      CategoryTheory.CategoryStruct.comp g f = h →
                        CategoryTheory.Limits.IsColimit
                          (CategoryTheory.Limits.CokernelCofork.ofπ (CategoryTheory.Limits.Cofork.π c) hf)
-- Mathlib.Geometry.Manifold.Algebra.Monoid
/-- Right multiplication by `g`. It is meant to mimic the usual notation in Lie groups.
Used mostly through the notation `𝑹`.
Lemmas involving `smoothRightMul` with the notation `𝑹` usually use `R` instead of `𝑹` in the
names.  -/
smoothRightMul : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {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 : Mul G] →
                    [inst_5 : TopologicalSpace G] →
                      [inst_6 : ChartedSpace H G] → G → [ContMDiffMul I (↑⊤) G] → ContMDiffMap I I G G ↑⊤
-- Mathlib.Algebra.Homology.Factorizations.CM5a
/-- The property that the second morphism of a factorisation is
an isomorphism in degrees `≤ n`.  -/
_private.Mathlib.Algebra.Homology.Factorizations.CM5a.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.isIsoLE : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {K L : CochainComplex C ℤ} →
        {f : K ⟶ L} →
          ℤ →
            CategoryTheory.ObjectProperty (CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.cofFib✝ f).FullSubcategory
-- Mathlib.CategoryTheory.MorphismProperty.Representable
CategoryTheory.MorphismProperty.relative_respectsIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} (P : CategoryTheory.MorphismProperty C),
  (CategoryTheory.MorphismProperty.relative F P).RespectsIso
-- Lean.Compiler.ExternAttr
Lean.ExternEntry.standard.injEq : ∀ (backend : Lean.Name) (fn : String) (backend_1 : Lean.Name) (fn_1 : String),
  (Lean.ExternEntry.standard backend fn = Lean.ExternEntry.standard backend_1 fn_1) = (backend = backend_1 ∧ fn = fn_1)
-- Mathlib.Data.Complex.Basic
Complex.ofReal_zpow : ∀ (r : ℝ) (n : ℤ), ↑(r ^ n) = ↑r ^ n
-- Mathlib.Data.NNReal.Defs
NNReal.coe_image : ∀ {s : Set NNReal}, NNReal.toReal '' s = {x | ∃ (h : 0 ≤ x), NNReal.mk x h ∈ s}
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
inv_mul_lt_iff_lt_mul : ∀ {α : Type u} [inst : Group α] [inst_1 : LT α] [MulLeftStrictMono α] {a b c : α}, b⁻¹ * a < c ↔ a < b * c
-- Mathlib.Algebra.Module.CharacterModule
TensorProduct.liftAddHom.congr_simp : ∀ {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]
  (f f_1 : M →+ N →+ P) (e_f : f = f_1) (hf : ∀ (r : R) (m : M) (n : N), (f (r • m)) n = (f m) (r • n)),
  TensorProduct.liftAddHom f hf = TensorProduct.liftAddHom f_1 ⋯
-- Mathlib.Tactic.ClickSuggestions.FindPremises
/-- The configuration used when indexing into the discrimination tree, and when looking up in it.

We do not reduce projections so that e.g. `Fin.val_mk : ⟨m, h⟩.val = m` can be indexed properly.

TODO?: projections should be reduced inside implicit arguments,
because otherwise we may reject some valid matches.
 -/
_private.Mathlib.Tactic.ClickSuggestions.FindPremises.0.Mathlib.Tactic.ClickSuggestions.librarySearchIndexConfig : Lean.Meta.Config
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.instHasKernelToSubtype : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {K : Type}
  [inst_2 : Finite K] [inst_3 : CategoryTheory.Limits.HasFiniteBiproducts C] (f : K → C) (p : K → Prop),
  CategoryTheory.Limits.HasKernel (CategoryTheory.Limits.biproduct.toSubtype f p)
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
IsUniformAddGroup.cauchy_iff_tendsto : ∀ {G : Type u_4} [inst : AddGroup G] [inst_1 : UniformSpace G] [IsUniformAddGroup G] (𝓕 : Filter G),
  Cauchy 𝓕 ↔ 𝓕.NeBot ∧ Filter.Tendsto (fun p => p.1 - p.2) (𝓕 ×ˢ 𝓕) (nhds 0)
-- Lean.DocString.Syntax
/-- Emphasis, often rendered as italics.

Emphasis may be nested by using longer sequences of `_` for the outer delimiters. For example:
```
Remember: __always butter the _rugbrød_ before adding toppings!__
```
Here, the outer `__` is used to emphasize the instructions, while the inner `_` indicates the use of
a non-English word.
 -/
Lean.Doc.Syntax.emph : Lean.ParserDescr
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instNeg : {G : Type u_1} → [inst : TopologicalSpace G] → [inst_1 : Neg G] → [ContinuousNeg G] → Neg (SeparationQuotient G)
-- Mathlib.CategoryTheory.Functor.KanExtension.Preserves
CategoryTheory.Functor.pointwiseRightKanExtensionCompIsoOfPreserves.eq_1 : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D] (G : CategoryTheory.Functor B D) (F : CategoryTheory.Functor A B)
  (L : CategoryTheory.Functor A C) [inst_4 : G.PreservesPointwiseRightKanExtension F L]
  [inst_5 : L.HasPointwiseRightKanExtension F],
  G.pointwiseRightKanExtensionCompIsoOfPreserves F L =
    ((L.pointwiseRightKanExtension F).comp G).rightKanExtensionUnique
      (CategoryTheory.CategoryStruct.comp (L.associator (L.pointwiseRightKanExtension F) G).inv
        (CategoryTheory.Functor.whiskerRight (L.pointwiseRightKanExtensionCounit F) G))
      (L.pointwiseRightKanExtension (F.comp G)) (L.pointwiseRightKanExtensionCounit (F.comp G))
-- Std.Http.Internal.Char
_private.Std.Http.Internal.Char.0.Std.Http.Internal.Char.quotedPairChar.match_1.eq_2 : ∀ (motive : Char → Sort u_1) (h_1 : Unit → motive '\t') (h_2 : Unit → motive ' ') (h_3 : (x : Char) → motive x),
  (match ' ' with
    | '\t' => h_1 ()
    | ' ' => h_2 ()
    | x => h_3 x) =
    h_2 ()
-- Mathlib.SetTheory.Ordinal.Basic
/-- `ω` is the first infinite ordinal, defined as the order type of `ℕ`. 

Conventions for notations in identifiers:

 * The recommended spelling of `ω` in identifiers is `omega0`. -/
Ordinal.termω : Lean.ParserDescr
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.imJ_smul : ∀ {S : Type u_1} {R : Type u_3} {c₁ c₂ c₃ : R} [inst : SMul S R] (s : S) (a : QuaternionAlgebra R c₁ c₂ c₃),
  (s • a).imJ = s • a.imJ
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
AlgHom.subalgebraMap_coe_apply : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Semiring B] [inst_4 : Algebra R B] {S : Subalgebra R A} (f : A →ₐ[R] B) (x : ↥S),
  ↑((AlgHom.subalgebraMap S f) x) = f ↑x
-- Mathlib.Data.List.MinMax
List.minimum_anti : ∀ {α : Type u_1} [inst : LinearOrder α] {l₁ l₂ : List α}, l₁ ⊆ l₂ → l₂.minimum ≤ l₁.minimum
-- Mathlib.GroupTheory.Perm.Fin
/-- `cycleIcc i j` is the cycle `(i i+1 ... j)` leaving `(0 ... i-1)` and `(j+1 ... n-1)`
unchanged when `i < j` and returning the dummy value `id` when `i > j`.
In other words, it rotates elements in `[i, j]` one step to the right.
 -/
Fin.cycleIcc : {n : ℕ} → Fin n → Fin n → Equiv.Perm (Fin n)
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.IsBasis.isBasis_closure_right : ∀ {α : Type u_2} {M : Matroid α} {X I : Set α}, M.IsBasis I X → M.IsBasis I (M.closure X)
-- Mathlib.NumberTheory.MulChar.Lemmas
MulChar.ofRootOfUnity.congr_simp : ∀ {M : Type u_1} [inst : CommMonoid M] [inst_1 : Fintype M] [inst_2 : DecidableEq M] {R : Type u_2}
  [inst_3 : CommMonoidWithZero R] {ζ ζ_1 : Rˣ} (e_ζ : ζ = ζ_1) (hζ : ζ ∈ rootsOfUnity (Fintype.card Mˣ) R) {g g_1 : Mˣ}
  (e_g : g = g_1) (hg : ∀ (x : Mˣ), x ∈ Subgroup.zpowers g), MulChar.ofRootOfUnity hζ hg = MulChar.ofRootOfUnity ⋯ ⋯
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Pretrivialization.target_eq : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  (self : Bundle.Pretrivialization F proj), self.target = self.baseSet ×ˢ Set.univ
-- Init.Data.Iterators.Lemmas.Combinators.Take
_private.Init.Data.Iterators.Lemmas.Combinators.Take.0.Std.Iter.toArray_eq_match_step.match_1.eq_3 : ∀ {α β : Type u_1} (motive : Std.IterStep (Std.Iter β) β → Sort u_2)
  (h_1 : (it' : Std.Iter β) → (out : β) → motive (Std.IterStep.yield it' out))
  (h_2 : (it' : Std.Iter β) → motive (Std.IterStep.skip it')) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.done with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it' => h_2 it'
    | Std.IterStep.done => h_3 ()) =
    h_3 ()
-- Init.Data.UInt.Basic
instMinUInt8 : Min UInt8
-- Mathlib.GroupTheory.MonoidLocalization.Basic
AddLocalization.mk_self_mk : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} (a : M) (haS : a ∈ S), AddLocalization.mk a ⟨a, haS⟩ = 0
-- Mathlib.LinearAlgebra.Lagrange
Lagrange.basisDivisor_inj : ∀ {F : Type u_1} [inst : Field F] {x y : F}, Lagrange.basisDivisor x y = 0 → x = y