mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Lie.Ideal
instIsLieTowerSubtypeMemLieIdeal : ∀ (R : Type u) (L : Type v) (M : Type w) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : LieRingModule L M] [inst_4 : LieAlgebra R L] (I : LieIdeal R L), IsLieTower (↥I) L M
-- Init.Data.List.Scan.Lemmas
List.scanl_reverse : ∀ {β : Type u_1} {α : Type u_2} {init : β} {f : β → α → β} {as : List α},
  List.scanl f init as.reverse = (List.scanr (flip f) init as).reverse
-- Mathlib.Analysis.Asymptotics.Lemmas
Asymptotics.isLittleO_mul_iff_isLittleO_div : ∀ {α : Type u_1} {𝕜 : Type u_15} [inst : NormedDivisionRing 𝕜] {l : Filter α} {f g h : α → 𝕜},
  (∀ᶠ (x : α) in l, f x ≠ 0) → ((fun x => f x * g x) =o[l] h ↔ g =o[l] fun x => h x / f x)
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Matrix.SpecialLinearGroup.hasInv : {n : Type u} →
  [inst : DecidableEq n] →
    [inst_1 : Fintype n] → {R : Type v} → [inst_2 : CommRing R] → Inv (Matrix.SpecialLinearGroup n R)
-- Mathlib.NumberTheory.LSeries.Dirichlet
DirichletCharacter.apply_eq_toArithmeticFunction_apply : ∀ {N : ℕ} {R : Type u_1} [inst : CommMonoidWithZero R] (χ : DirichletCharacter R N) {n : ℕ},
  n ≠ 0 → χ ↑n = (toArithmeticFunction fun x => χ ↑x) n
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.SolverExtension.internalize : {σ : Type} → Lean.Meta.Grind.SolverExtension σ → Lean.Expr → Option Lean.Expr → Lean.Meta.Grind.GoalM Unit
-- Init.Data.Option.Basic
instMonadOption : Monad Option
-- Mathlib.Computability.PartrecCode
_private.Mathlib.Computability.PartrecCode.0.Nat.Partrec.Code.ofNatCode.match_3.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : Unit → motive 1) (h_3 : Unit → motive 2)
  (h_4 : Unit → motive 3) (h_5 : (n : ℕ) → motive n.succ.succ.succ.succ),
  (match 0 with
    | 0 => h_1 ()
    | 1 => h_2 ()
    | 2 => h_3 ()
    | 3 => h_4 ()
    | n.succ.succ.succ.succ => h_5 n) =
    h_1 ()
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.map_map_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S S' : D} {T : CategoryTheory.Functor C D} (f : S ⟶ S')
  {X Y : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit S') T} (f_1 : X ⟶ Y),
  ((CategoryTheory.StructuredArrow.map f).map f_1).left = CategoryTheory.CategoryStruct.id X.left
-- Batteries.Data.List.Lemmas
List.finRange_eq_pmap_range : ∀ {n : ℕ}, List.finRange n = List.pmap Fin.mk (List.range n) ⋯
-- Mathlib.Combinatorics.Graph.Basic
Graph.Compatible.of_disjoint_edgeSet : ∀ {α : Type u_1} {β : Type u_2} {G H : Graph α β}, Disjoint G.edgeSet H.edgeSet → G.Compatible H
-- Mathlib.CategoryTheory.Localization.Predicate
CategoryTheory.Localization.Lifting.ofIsos_iso : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (L : CategoryTheory.Functor C D)
  (W : CategoryTheory.MorphismProperty C) {E : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  {F₁ F₂ : CategoryTheory.Functor C E} {F₁' F₂' : CategoryTheory.Functor D E} (e : F₁ ≅ F₂) (e' : F₁' ≅ F₂')
  [inst_3 : CategoryTheory.Localization.Lifting L W F₁ F₁'],
  CategoryTheory.Localization.Lifting.iso L W F₂ F₂' =
    L.isoWhiskerLeft e'.symm ≪≫ CategoryTheory.Localization.Lifting.iso L W F₁ F₁' ≪≫ e
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
/-- If `f : X → R → R` is continuous on `s : Set X` in the topology on
`X → R →ᵤ[{spectrum R a}] → R`, and each `f` is continuous on the spectrum, then `x ↦ cfc (f x) a`
is continuous on `s` also.  -/
ContinuousOn.cfc_fun : ∀ {X : Type u_1} {R : Type u_2} {A : Type u_3} {p : A → Prop} [inst : CommSemiring R] [inst_1 : StarRing R]
  [inst_2 : MetricSpace R] [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : Ring A]
  [inst_6 : StarRing A] [inst_7 : TopologicalSpace A] [inst_8 : Algebra R A]
  [inst_9 : ContinuousFunctionalCalculus R A p] [inst_10 : TopologicalSpace X] {f : X → R → R} {a : A} {s : Set X},
  ContinuousOn (fun x => (UniformOnFun.ofFun {spectrum R a}) (f x)) s →
    autoParam (∀ x ∈ s, ContinuousOn (f x) (spectrum R a)) ContinuousOn.cfc_fun._auto_1 →
      ContinuousOn (fun x => cfc (f x) a) s
-- Mathlib.Analysis.Normed.Unbundled.SpectralNorm
/-- The spectral norm extends the norm on `K`.  -/
spectralNorm_extends : ∀ {K : Type u_2} [inst : NormedField K] {L : Type u_3} [inst_1 : Field L] [inst_2 : Algebra K L] (k : K),
  spectralNorm K L ((algebraMap K L) k) = ‖k‖
-- Mathlib.Order.Filter.Basic
Filter.EventuallyEq.symm : ∀ {α : Type u} {β : Type v} {f g : α → β} {l : Filter α}, f =ᶠ[l] g → g =ᶠ[l] f
-- Mathlib.Order.Hom.Lattice
InfHomClass.mk : ∀ {F : Type u_6} {α : Type u_7} {β : Type u_8} [inst : Min α] [inst_1 : Min β] [inst_2 : FunLike F α β],
  (∀ (f : F) (a b : α), f (a ⊓ b) = f a ⊓ f b) → InfHomClass F α β
-- Mathlib.CategoryTheory.Monoidal.Center
CategoryTheory.Center.ofBraided_obj : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X : C),
  (CategoryTheory.Center.ofBraided C).obj X = CategoryTheory.Center.ofBraidedObj X
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Append
Std.Tactic.BVDecide.BVExpr.bitblast.blastAppend.eq_1 : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {newWidth : ℕ} (aig : Std.Sat.AIG α) (lw rw : ℕ)
  (lhs : aig.RefVec lw) (rhs : aig.RefVec rw) (h : newWidth = rw + lw),
  Std.Tactic.BVDecide.BVExpr.bitblast.blastAppend aig { lw := lw, rw := rw, lhs := lhs, rhs := rhs, h := h } =
    { aig := aig, vec := ⋯ ▸ rhs.append lhs }
-- Mathlib.RingTheory.TensorProduct.Maps
Algebra.TensorProduct.mapOfCompatibleSMul_tmul : ∀ (R : Type u_3) (S : Type u_4) (T : Type u_5) (A : Type u_6) (B : Type u_7) [inst : CommSemiring R]
  [inst_1 : CommSemiring S] [inst_2 : CommSemiring T] [inst_3 : Semiring A] [inst_4 : Semiring B] [inst_5 : Algebra R A]
  [inst_6 : Algebra R B] [inst_7 : Algebra S A] [inst_8 : Algebra S B] [inst_9 : Algebra T A]
  [inst_10 : SMulCommClass R T A] [inst_11 : SMulCommClass S T A] [inst_12 : SMulCommClass R S A]
  [inst_13 : TensorProduct.CompatibleSMul R S A B] (m : A) (n : B),
  (Algebra.TensorProduct.mapOfCompatibleSMul R S T A B) (m ⊗ₜ[S] n) = m ⊗ₜ[R] n
-- Init.Grind.Ordered.Module
/-- Addition is compatible with a preorder if `a ≤ b ↔ a + c ≤ b + c`.
 -/
Lean.Grind.OrderedAdd : (M : Type u) → [HAdd M M M] → [inst : LE M] → [Std.IsPreorder M] → Prop
-- Mathlib.Data.Nat.Periodic
/-- An interval of length `a` filtered over a periodic predicate of period `a` has cardinality
equal to the number naturals below `a` for which `p a` is true.  -/
Nat.filter_multiset_Ico_card_eq_of_periodic : ∀ (n a : ℕ) (p : ℕ → Prop) [inst : DecidablePred p],
  Function.Periodic p a → (Multiset.filter p (Multiset.Ico n (n + a))).card = Nat.count p a
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Grp.mk.inj : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.CartesianMonoidalCategory C}
  {X : C} {grp : CategoryTheory.GrpObj X} {X_1 : C} {grp_1 : CategoryTheory.GrpObj X_1},
  { X := X, grp := grp } = { X := X_1, grp := grp_1 } → X = X_1 ∧ grp ≍ grp_1
-- Mathlib.Order.Filter.Basic
Filter.mem_inf_of_inter : ∀ {α : Type u} {f g : Filter α} {s t u : Set α}, s ∈ f → t ∈ g → s ∩ t ⊆ u → u ∈ f ⊓ g
-- Init.Notation
/-- Boolean “or”, also known as disjunction. `or x y` can be written `x || y`.

The corresponding propositional connective is `Or : Prop → Prop → Prop`, written with the `∨`
operator.

The Boolean `or` is a `@[macro_inline]` function in order to give it short-circuiting evaluation:
if `x` is `true` then `y` is not evaluated at runtime.


Conventions for notations in identifiers:

 * The recommended spelling of `||` in identifiers is `or`. -/
«term_||_» : Lean.TrailingParserDescr
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
CategoryTheory.Limits.colimitCompWhiskeringLeftIsoCompColimit.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {J : Type u₁} [inst_2 : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂}
  [inst_3 : CategoryTheory.Category.{v₂, u₂} K] (F : CategoryTheory.Functor J (CategoryTheory.Functor K C))
  (G : CategoryTheory.Functor D K) [inst_4 : CategoryTheory.Limits.HasColimitsOfShape J C],
  CategoryTheory.Limits.colimitCompWhiskeringLeftIsoCompColimit F G =
    CategoryTheory.NatIso.ofComponents
      (fun j =>
        CategoryTheory.Limits.colimitObjIsoColimitCompEvaluation
            (F.comp ((CategoryTheory.Functor.whiskeringLeft D K C).obj G)) j ≪≫
          CategoryTheory.Limits.HasColimit.isoOfNatIso
              (F.isoWhiskerLeft (CategoryTheory.whiskeringLeftCompEvaluation G j)) ≪≫
            (CategoryTheory.Limits.colimitObjIsoColimitCompEvaluation F (G.obj j)).symm)
      ⋯
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey!_filter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {f : α → β → Bool} {k : α},
  (Std.ExtTreeMap.filter f t).getKey! k = ((t.getKey? k).pfilter fun x h' => f x t[x]).get!
-- Mathlib.LinearAlgebra.TensorPower.Basic
/-- Homogeneous tensor powers $M^{\otimes n}$. `⨂[R]^n M` is a shorthand for
`⨂[R] (i : Fin n), M`.  -/
TensorPower : (R : Type u_1) →
  ℕ → (M : Type u_2) → [inst : CommSemiring R] → [inst_1 : AddCommMonoid M] → [Module R M] → Type (max u_2 u_1)
-- Mathlib.Topology.Algebra.ContinuousAffineMap
ContinuousAffineMap.contLinear.congr_simp : ∀ {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} {Q : Type u_5} [inst : Ring R] [inst_1 : AddCommGroup V]
  [inst_2 : Module R V] [inst_3 : TopologicalSpace P] [inst_4 : AddTorsor V P] [inst_5 : AddCommGroup W]
  [inst_6 : Module R W] [inst_7 : TopologicalSpace Q] [inst_8 : AddTorsor W Q] [inst_9 : TopologicalSpace V]
  [inst_10 : IsTopologicalAddTorsor P] [inst_11 : TopologicalSpace W] [inst_12 : IsTopologicalAddTorsor Q]
  (f f_1 : P →ᴬ[R] Q), f = f_1 → f.contLinear = f_1.contLinear
-- Mathlib.CategoryTheory.Localization.Predicate
CategoryTheory.Localization.uniq_symm : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D₁ : Type u_4} {D₂ : Type u_5}
  [inst_1 : CategoryTheory.Category.{v_4, u_4} D₁] [inst_2 : CategoryTheory.Category.{v_5, u_5} D₂]
  (L₁ : CategoryTheory.Functor C D₁) (L₂ : CategoryTheory.Functor C D₂) (W' : CategoryTheory.MorphismProperty C)
  [inst_3 : L₁.IsLocalization W'] [inst_4 : L₂.IsLocalization W'],
  (CategoryTheory.Localization.uniq L₁ L₂ W').symm = CategoryTheory.Localization.uniq L₂ L₁ W'
-- Mathlib.Order.BooleanAlgebra.Basic
himp_le_left : ∀ {α : Type u} {x y : α} [inst : BooleanAlgebra α], x ⇨ y ≤ x ↔ x = ⊤
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.maxKeyD_mem : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → t.isEmpty = false → ∀ {fallback : α}, t.maxKeyD fallback ∈ t
-- Mathlib.Data.Set.Countable
Set.countable_coe_iff : ∀ {α : Type u} {s : Set α}, Countable ↑s ↔ s.Countable
-- Mathlib.NumberTheory.NumberField.Completion.FinitePlace
NumberField.HeightOneSpectrum.embedding_mul_absNorm : ∀ (K : Type u_1) [inst : Field K] {R : Type u_2} [inst_1 : CommRing R] [inst_2 : Algebra R K]
  [inst_3 : IsDedekindDomain R] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R)
  [inst_5 : Module.Finite ℤ R] [inst_6 : Module.Free ℤ R] {x : R},
  x ≠ 0 →
    ‖(NumberField.FinitePlace.embedding v) ((algebraMap R K) x)‖ *
        ↑(Ideal.absNorm (v.maxPowDividing (Ideal.span {x}))) =
      1
-- Mathlib.Data.ENNReal.Inv
ENNReal.monotone_zpow : ∀ {x : ENNReal}, 1 ≤ x → Monotone fun x_1 => x ^ x_1
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
tangentMapWithin_proj : ∀ {𝕜 : 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] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {s : Set M}
  {p : TangentBundle I M}, (tangentMapWithin I I' f s p).proj = f p.proj
-- Mathlib.Topology.OpenPartialHomeomorph.Defs
OpenPartialHomeomorph.eq_symm_apply : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y) {x : X} {y : Y}, x ∈ e.source → y ∈ e.target → (x = ↑e.symm y ↔ ↑e x = y)
-- Aesop.Search.Expansion
Aesop.SafeRuleResult.isSuccessfulOrPostponed : Aesop.SafeRuleResult → Bool
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.mapComp_id_right_hom_app_assoc : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {a b : B}
  (f : a ⟶ b) (X : ↑(F.obj a)) {Z : ↑(F.obj b)}
  (h : (F.map (CategoryTheory.CategoryStruct.id b)).toFunctor.obj ((F.map f).toFunctor.obj X) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((F.mapComp f (CategoryTheory.CategoryStruct.id b)).hom.toNatTrans.app X) h =
    CategoryTheory.CategoryStruct.comp ((F.map₂ (CategoryTheory.Bicategory.rightUnitor f).hom).toNatTrans.app X)
      (CategoryTheory.CategoryStruct.comp ((F.mapId b).inv.toNatTrans.app ((F.map f).toFunctor.obj X)) h)
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.RingEqCnstrProof.symm.injEq : ∀ (c c_1 : Lean.Meta.Grind.Arith.Linear.RingEqCnstr),
  (Lean.Meta.Grind.Arith.Linear.RingEqCnstrProof.symm c = Lean.Meta.Grind.Arith.Linear.RingEqCnstrProof.symm c_1) =
    (c = c_1)
-- Mathlib.Topology.Algebra.Group.Basic
Continuous.of_coeHom_comp : ∀ {G : Type w} {H : Type x} [inst : Group G] [inst_1 : Monoid H] [inst_2 : TopologicalSpace G]
  [inst_3 : TopologicalSpace H] [ContinuousInv G] {f : G →* Hˣ}, Continuous ⇑((Units.coeHom H).comp f) → Continuous ⇑f
-- Mathlib.Algebra.Group.Hom.Basic
MonoidHom.mul_comp : ∀ {M : Type u_2} {N : Type u_3} {P : Type u_4} [inst : MulOneClass M] [inst_1 : CommMonoid N] [inst_2 : MulOneClass P]
  (g₁ g₂ : M →* N) (f : P →* M), (g₁ * g₂).comp f = g₁.comp f * g₂.comp f
-- Lean.Elab.ConfigEval.Types
/-- An evaluator for updating a configuration object using configuration items.

This is not a class. In practice, it might be composed out of evaluators or otherwise parameterized in a number of ways.
 -/
Lean.Elab.ConfigEval.EvalConfigItem : Type → Type
-- Mathlib.CategoryTheory.Discrete.Basic
CategoryTheory.Discrete.exists : ∀ {α : Type u_1} {p : CategoryTheory.Discrete α → Prop}, (∃ a, p a) ↔ ∃ a', p { as := a' }
-- Mathlib.Order.Filter.AtTopBot.Disjoint
Filter.disjoint_atBot_principal_Ioi : ∀ {α : Type u_3} [inst : Preorder α] (x : α), Disjoint Filter.atBot (Filter.principal (Set.Ioi x))
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.sub_apply : ∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → AddGroup (β i)] (g₁ g₂ : Π₀ (i : ι), β i) (i : ι),
  (g₁ - g₂) i = g₁ i - g₂ i
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.get_ofList_of_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp] [inst : Std.LawfulEqCmp cmp]
  {l : List ((a : α) × β a)} {k k' : α} (k_eq : cmp k k' = Ordering.eq) {v : β k},
  List.Pairwise (fun a b => ¬cmp a.fst b.fst = Ordering.eq) l →
    ⟨k, v⟩ ∈ l → ∀ {h : k' ∈ Std.DTreeMap.Raw.ofList l cmp}, (Std.DTreeMap.Raw.ofList l cmp).get k' h = cast ⋯ v
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.tensorObj_zero : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X Y : CategoryTheory.AddMon C),
  CategoryTheory.AddMonObj.zero =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv
      (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.AddMonObj.zero CategoryTheory.AddMonObj.zero)
-- Mathlib.Data.EReal.Inv
EReal.bot_div_of_neg_ne_bot : ∀ {a : EReal}, a < 0 → a ≠ ⊥ → ⊥ / a = ⊤
-- Mathlib.LinearAlgebra.BilinearMap
LinearMap.map_smul₂ : ∀ {R : Type u_1} {S : Type u_3} {S₂ : Type u_4} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : Semiring S₂]
  {M₂ : Type u_6} {N₂ : Type u_8} {P₂ : Type u_10} [inst_3 : AddCommMonoid M₂] [inst_4 : AddCommMonoid N₂]
  [inst_5 : AddCommMonoid P₂] [inst_6 : Module R M₂] [inst_7 : Module S N₂] [inst_8 : Module R P₂]
  [inst_9 : Module S₂ P₂] [inst_10 : SMulCommClass S₂ R P₂] {σ₁₂ : S →+* S₂} (f : M₂ →ₗ[R] N₂ →ₛₗ[σ₁₂] P₂) (r : R)
  (x : M₂) (y : N₂), (f (r • x)) y = r • (f x) y
-- Mathlib.CategoryTheory.Comma.Arrow
CategoryTheory.Arrow.homMk'_right : ∀ {T : Type u} [inst : CategoryTheory.Category.{v, u} T] {X Y : T} {f : X ⟶ Y} {P Q : T} {g : P ⟶ Q} (u : X ⟶ P)
  (v : Y ⟶ Q)
  (w :
    autoParam (CategoryTheory.CategoryStruct.comp u g = CategoryTheory.CategoryStruct.comp f v)
      CategoryTheory.Arrow.homMk'._auto_1),
  (CategoryTheory.Arrow.homMk' u v w).right = v
-- Init.Data.Order.Ord
Std.TransCmp.lt_trans : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {a b c : α},
  cmp a b = Ordering.lt → cmp b c = Ordering.lt → cmp a c = Ordering.lt
-- Mathlib.Tactic.Translate.GuessName
Mathlib.Tactic.GuessName.GuessNameData.mk.sizeOf_spec : ∀ (nameDict : Std.HashMap String (List String)) (abbreviationDict : Std.HashMap String String),
  sizeOf { nameDict := nameDict, abbreviationDict := abbreviationDict } = 1 + sizeOf nameDict + sizeOf abbreviationDict
-- Mathlib.CategoryTheory.Action.Basic
Action.functorCategoryEquivalence_unitIso : ∀ (V : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} V] (G : Type u_2) [inst_1 : Monoid G],
  (Action.functorCategoryEquivalence V G).unitIso = Action.FunctorCategoryEquivalence.unitIso
-- Init.Data.Order.MinMaxOn
minOn_id : ∀ {α : Type u_1} [inst : Min α] [inst_1 : LE α] [inst_2 : DecidableLE α] [Std.LawfulOrderLeftLeaningMin α] {x y : α},
  minOn id x y = x ⊓ y
-- Mathlib.Data.Multiset.Fintype
Multiset.instIsEmptyToTypeEmptyCollection : ∀ {α : Type u_1} [inst : DecidableEq α], IsEmpty ∅.ToType
-- Mathlib.Topology.EMetricSpace.Pi
/-- The product of a finite number of emetric spaces, with the max distance, is still
an emetric space.
This construction would also work for infinite products, but it would not give rise
to the product topology. Hence, we only formalize it in the good situation of finitely many
spaces.  -/
emetricSpacePi : {β : Type v} → {X : β → Type u_2} → [Fintype β] → [(b : β) → EMetricSpace (X b)] → EMetricSpace ((b : β) → X b)
-- Mathlib.Algebra.Group.Indicator
Set.mulSupport_subset_subsingleton_of_disjoint_on_mulSupport : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : One β] {s : γ → Set α} (f : α → β),
  Pairwise (Function.onFun Disjoint fun j => s j ∩ Function.mulSupport f) →
    ∀ (i : α) (j : γ), i ∈ s j → (Function.mulSupport fun d => (s d).mulIndicator f i) ⊆ {j}
-- Mathlib.Order.Interval.Set.WithBotTop
WithBot.Ioc_coe : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, Set.Ioc ↑b ↑a = WithBot.some '' Set.Ioc b a
-- Mathlib.Algebra.CharP.Defs
CharP.ofCharZero : ∀ (R : Type u_1) [inst : AddMonoidWithOne R] [CharZero R], CharP R 0
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.Code.cons.sizeOf_spec : ∀ (a a_1 : Turing.ToPartrec.Code), sizeOf (a.cons a_1) = 1 + sizeOf a + sizeOf a_1
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.Exact.mono_g' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S : CategoryTheory.ShortComplex C}, S.Exact → ∀ (h : S.RightHomologyData), CategoryTheory.Mono h.g'
-- Mathlib.Order.LiminfLimsup
Filter.HasBasis.liminf_eq_iSup_iInf : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : CompleteLattice α] {p : ι → Prop} {s : ι → Set β} {f : Filter β}
  {u : β → α}, f.HasBasis p s → Filter.liminf u f = ⨆ i, ⨆ (_ : p i), ⨅ a ∈ s i, u a
-- Lean.Meta.Hint
_private.Lean.Meta.Hint.0.Lean.Meta.Hint.readableDiff.splitWords : String → Array String × Array String
-- Mathlib.Analysis.Normed.Unbundled.SpectralNorm
/-- The spectral norm is nonarchimedean when `L/K` is finite and normal.
See also `isNonarchimedean_spectralNorm` for a more general result.  -/
isNonarchimedean_spectralNorm_of_finiteDimensional_normal : ∀ (K : Type u_2) [inst : NormedField K] (L : Type u_3) [inst_1 : Field L] [inst_2 : Algebra K L]
  [h_fin : FiniteDimensional K L] [hn : Normal K L] [IsUltrametricDist K], IsNonarchimedean (spectralNorm K L)
-- Init.Data.Float.Model.Unpacked.Round
/-- The bitwise `or` of all bits that are even less significant than the round bit.   -/
Float.Model.UnpackedFloat.ExtendedMantissa.stickyBit : Float.Model.UnpackedFloat.ExtendedMantissa → Bool
-- Mathlib.RingTheory.PowerSeries.Substitution
PowerSeries.HasSubst.monomial : ∀ {τ : Type u_3} {S : Type u_4} [inst : CommRing S] {n : τ →₀ ℕ},
  n ≠ 0 → ∀ (s : S), PowerSeries.HasSubst ((MvPowerSeries.monomial n) s)
-- Mathlib.CategoryTheory.Sites.IsSheafFor
/-- A more explicit version of `FamilyOfElements.Compatible` for a `Presieve.ofArrows`.
 -/
CategoryTheory.Presieve.Arrows.Compatible : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (P : CategoryTheory.Functor Cᵒᵖ (Type w)) →
      {B : C} → {I : Type u_1} → {X : I → C} → ((i : I) → X i ⟶ B) → ((i : I) → P.obj (Opposite.op (X i))) → Prop
-- Mathlib.CategoryTheory.Action.Continuous
instCategoryDiscreteContAction : (V : Type u_2) →
  [inst : CategoryTheory.Category.{u_1, u_2} V] →
    {FV : V → V → Type u_4} →
      {CV : V → Type u_5} →
        [inst_1 : (X Y : V) → FunLike (FV X Y) (CV X) (CV Y)] →
          [inst_2 : CategoryTheory.ConcreteCategory V FV] →
            [inst_3 : CategoryTheory.HasForget₂ V TopCat] →
              (G : Type u_3) →
                [inst_4 : Monoid G] →
                  [inst_5 : TopologicalSpace G] →
                    CategoryTheory.Category.{u_1, max (max u_2 u_3) u_1} (DiscreteContAction V G)
-- Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone
CategoryTheory.SmallObject.SuccStruct.arrowMap_ofCocone_to_top : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {J : Type u} [inst_1 : LinearOrder J] {j : J}
  {F : CategoryTheory.Functor (↑(Set.Iio j)) C} (c : CategoryTheory.Limits.Cocone F) (i : J) (hi : i < j),
  CategoryTheory.SmallObject.SuccStruct.arrowMap (CategoryTheory.SmallObject.SuccStruct.ofCocone c) i j ⋯ ⋯ =
    CategoryTheory.Arrow.mk (c.ι.app ⟨i, hi⟩)
-- Std.Data.TreeMap.Basic
/-- Inserts multiple mappings into the tree map by iterating over the given collection and calling
`insert`. If the same key appears multiple times, the last occurrence takes precedence.

Note: this precedence behavior is true for `TreeMap`, `DTreeMap`, `TreeMap.Raw` and `DTreeMap.Raw`.
The `insertMany` function on `TreeSet` and `TreeSet.Raw` behaves differently: it will prefer the first
appearance.
 -/
Std.TreeMap.insertMany : {α : Type u} →
  {β : Type v} →
    {cmp : α → α → Ordering} → {ρ : Type u_1} → [ForIn Id ρ (α × β)] → Std.TreeMap α β cmp → ρ → Std.TreeMap α β cmp
-- Init.Meta.Defs
Lean.TSyntax.instCoeStrLitTerm : Coe Lean.StrLit Lean.Term
-- Init.Grind.Norm
Lean.Grind.not_implies : ∀ (p q : Prop), (¬(p → q)) = (p ∧ ¬q)
-- Mathlib.Topology.Algebra.Monoid
continuous_finsetProd : ∀ {ι : Type u_1} {M : Type u_3} {X : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace M]
  [inst_2 : CommMonoid M] [ContinuousMul M] {f : ι → X → M} (s : Finset ι),
  (∀ i ∈ s, Continuous (f i)) → Continuous fun a => ∏ i ∈ s, f i a
-- Mathlib.Analysis.Normed.Module.Ball.Homeomorph
OpenPartialHomeomorph.univBall_apply_zero : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {P : Type u_2}
  [inst_2 : PseudoMetricSpace P] [inst_3 : NormedAddTorsor E P] (c : P) (r : ℝ),
  ↑(OpenPartialHomeomorph.univBall c r) 0 = c
-- Batteries.Data.Nat.Bitwise.Lemmas
Nat.and_right_comm : ∀ (x y z : ℕ), x &&& y &&& z = x &&& z &&& y