mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Localization.Module
LocalizedModule.map_id : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) {M : Type u_2} [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M], (LocalizedModule.map S) LinearMap.id = LinearMap.id
-- Lean.LocalContext
Lean.LocalContext.replaceFVarId : Lean.FVarId → Lean.Expr → Lean.LocalContext → Lean.LocalContext
-- Mathlib.CategoryTheory.Monoidal.Discrete
CategoryTheory.Discrete.monoidal.eq_1 : ∀ (M : Type u) [inst : Monoid M],
  CategoryTheory.Discrete.monoidal M =
    { tensorObj := fun X Y => { as := X.as * Y.as }, whiskerLeft := fun X x x_1 f => CategoryTheory.eqToHom ⋯,
      whiskerRight := fun {X₁ X₂} f X => CategoryTheory.eqToHom ⋯,
      tensorHom := fun {X₁ Y₁ X₂ Y₂} f g => CategoryTheory.eqToHom ⋯, tensorUnit := { as := 1 },
      associator := fun x x_1 x_2 => CategoryTheory.Discrete.eqToIso ⋯,
      leftUnitor := fun X => CategoryTheory.Discrete.eqToIso ⋯,
      rightUnitor := fun X => CategoryTheory.Discrete.eqToIso ⋯, tensorHom_def := ⋯, id_tensorHom_id := ⋯,
      tensorHom_comp_tensorHom := ⋯, whiskerLeft_id := ⋯, id_whiskerRight := ⋯, associator_naturality := ⋯,
      leftUnitor_naturality := ⋯, rightUnitor_naturality := ⋯, pentagon := ⋯, triangle := ⋯ }
-- Mathlib.Tactic.Positivity.Basic
/-- **Alias** of the reverse direction of `Rat.num_pos`. -/
Mathlib.Meta.Positivity.num_pos_of_pos : ∀ {a : ℚ}, 0 < a → 0 < a.num
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.State.toIntInfos : Lean.Meta.Grind.Arith.Cutsat.State → Lean.PArray Lean.Meta.Grind.Arith.Cutsat.ToIntInfo
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey?_insert_self : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {v : β}, (m.insert k v).getKey? k = some k
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
MeasureTheory.condExpInd_disjoint_union_apply : ∀ {α : Type u_1} {G : Type u_4} [inst : NormedAddCommGroup G] {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {s t : Set α} [inst_1 : NormedSpace ℝ G] {hm : m ≤ m0} [inst_2 : MeasureTheory.SigmaFinite (μ.trim hm)],
  MeasurableSet s →
    MeasurableSet t →
      μ s ≠ ⊤ →
        μ t ≠ ⊤ →
          Disjoint s t →
            ∀ (x : G),
              (MeasureTheory.condExpInd G hm μ (s ∪ t)) x =
                (MeasureTheory.condExpInd G hm μ s) x + (MeasureTheory.condExpInd G hm μ t) x
-- Mathlib.Order.Interval.Set.Basic
/-- **Alias** of `Set.Icc_sdiff_both`. -/
Set.Icc_diff_both : ∀ {α : Type u_1} [inst : PartialOrder α] {a b : α}, Set.Icc a b \ {a, b} = Set.Ioo a b
-- Mathlib.CategoryTheory.SmallRepresentatives
/-- identity morphisms  -/
CategoryTheory.SmallCategoryOfSet.id : {Ω : Type w} → (self : CategoryTheory.SmallCategoryOfSet Ω) → (X : ↑self.obj) → ↑(self.hom X X)
-- Mathlib.GroupTheory.GroupAction.Basic
IsCancelVAdd.stabilizer_eq_bot : ∀ {G : Type u_1} {α : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] [IsCancelVAdd G α] (a : α),
  AddAction.stabilizer G a = ⊥
-- Mathlib.MeasureTheory.Integral.Lebesgue.Basic
MeasureTheory.lintegral_mono_nnreal : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : α → NNReal},
  f ≤ g → ∫⁻ (a : α), ↑(f a) ∂μ ≤ ∫⁻ (a : α), ↑(g a) ∂μ
-- Std.Do.WP.Sound
_private.Std.Do.WP.Sound.0.Std.Do.instWPSoundExceptTExceptPureOfLawfulMonad.match_1.splitter : {ε α : Type u_1} →
  (motive : Except ε α → Sort u_2) →
    (r : Except ε α) → ((a : α) → motive (Except.ok a)) → ((a : ε) → motive (Except.error a)) → motive r
-- Mathlib.Topology.Algebra.RestrictedProduct.Units
RestrictedProduct.coe_unitsEquiv_apply : ∀ {ι : Type u_1} {R : ι → Type u_2} [inst : (i : ι) → Monoid (R i)] {S : ι → Type u_3}
  [inst_1 : (i : ι) → SetLike (S i) (R i)] [inst_2 : ∀ (i : ι), SubmonoidClass (S i) (R i)] {B : (i : ι) → S i}
  {𝓕 : Filter ι} (x : (RestrictedProduct (fun i => R i) (fun i => ↑(B i)) 𝓕)ˣ) (i : ι),
  ↑((RestrictedProduct.unitsEquiv R) x) i = ((RestrictedProduct.unitsEquiv R) x) i
-- Init.Data.ToString.Name
Lean.Name.instToString : ToString Lean.Name
-- Mathlib.SetTheory.Lists
/-- Predicate stating that a ZFA list is proper.  -/
Lists.IsList : {α : Type u_1} → Lists α → Prop
-- Mathlib.Order.Filter.Pointwise
Filter.one_neBot : ∀ {α : Type u_2} [inst : One α], Filter.NeBot 1
-- Init.Data.Range.Polymorphic.SInt
_private.Init.Data.Range.Polymorphic.SInt.0.HasModel.instRxiLawfulHasSize : ∀ {α : Type u} [inst : LE α] [inst_1 : LT α] {β : Type v} [inst_2 : LE β] [inst_3 : LT β]
  [inst_4 : Std.PRange.UpwardEnumerable β] [inst_5 : Std.PRange.LawfulUpwardEnumerable β]
  [inst_6 : Std.PRange.LawfulUpwardEnumerableLE β] [inst_7 : Std.PRange.LawfulUpwardEnumerableLT β] [m : HasModel✝ α β]
  [inst_8 : Std.Rxi.HasSize β] [Std.Rxi.LawfulHasSize β], Std.Rxi.LawfulHasSize α
-- Mathlib.Topology.Algebra.InfiniteSum.Order
lt_hasProd : ∀ {ι : Type u_1} {α : Type u_3} {L : SummationFilter ι} [inst : CommMonoid α] [inst_1 : Preorder α] [IsOrderedMonoid α]
  [inst_3 : TopologicalSpace α] [OrderClosedTopology α] {f : ι → α} {a : α} [L.NeBot] [L.LeAtTop]
  [MulRightStrictMono α], HasProd f a L → ∀ (i : ι), (∀ (j : ι), j ≠ i → 1 ≤ f j) → ∀ (j : ι), j ≠ i → 1 < f j → f i < a
-- Mathlib.Algebra.Module.Submodule.Basic
Submodule.notMem_of_ortho : ∀ {R : Type u} {M : Type v} [inst : Ring R] [IsDomain R] [inst_2 : AddCommGroup M] [inst_3 : Module R M] {x : M}
  {N : Submodule R M}, (∀ (c : R), ∀ y ∈ N, c • x + y = 0 → c = 0) → x ∉ N
-- Mathlib.Algebra.Category.Semigrp.Basic
Semigrp.forgetReflectsIsos : (CategoryTheory.forget Semigrp).ReflectsIsomorphisms
-- Mathlib.Algebra.Group.Equiv.Defs
MulHom.toMulEquiv_apply : ∀ {M : Type u_4} {N : Type u_5} [inst : Mul M] [inst_1 : Mul N] (f : M →ₙ* N) (g : N →ₙ* M)
  (h₁ : g.comp f = MulHom.id M) (h₂ : f.comp g = MulHom.id N), ⇑(f.toMulEquiv g h₁ h₂) = ⇑f
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.Solvers.check : Lean.Meta.Grind.GoalM Bool
-- Mathlib.Algebra.Module.Rat
SMulCommClass.rat' : ∀ {α : Type u} {M : Type v} [inst : AddCommGroup M] [inst_1 : DistribSMul α M] [inst_2 : Module ℚ M],
  SMulCommClass α ℚ M
-- Mathlib.Algebra.GroupWithZero.Action.Units
Units.instDistribMulAction : {M : Type u_3} →
  {α : Type u_4} → [inst : Monoid M] → [inst_1 : AddMonoid α] → [DistribMulAction M α] → DistribMulAction Mˣ α
-- Mathlib.Data.Ordmap.Invariants
_private.Mathlib.Data.Ordmap.Invariants.0.Ordnode.findMax'.match_1.eq_1 : ∀ {α : Type u_1} (motive : α → Ordnode α → Sort u_2) (x : α) (h_1 : (x : α) → motive x Ordnode.nil)
  (h_2 : (x : α) → (size : ℕ) → (l : Ordnode α) → (x_1 : α) → (r : Ordnode α) → motive x (Ordnode.node size l x_1 r)),
  (match x, Ordnode.nil with
    | x, Ordnode.nil => h_1 x
    | x, Ordnode.node size l x_1 r => h_2 x size l x_1 r) =
    h_1 x
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
/-- The function `ℤ ^ 2 → ℝ` given by `x ↦ ‖x‖ ^ (-k)` is summable if `2 < k`. We prove this by
splitting into boxes using `Finset.box`.  -/
EisensteinSeries.summable_one_div_norm_rpow : ∀ {k : ℝ}, 2 < k → Summable fun x => ‖x‖ ^ (-k)
-- Mathlib.RingTheory.TwoSidedIdeal.Basic
TwoSidedIdeal.mul_mem_right : ∀ {R : Type u_1} [inst : NonUnitalNonAssocRing R] (I : TwoSidedIdeal R) (x y : R), x ∈ I → x * y ∈ I
-- Init.Data.Nat.Lemmas
Nat.div_add_mod' : ∀ (a b : ℕ), a / b * b + a % b = a
-- Lean.Meta.Sym.LitValues
Lean.Meta.Sym.getRatValue? : Lean.Expr → OptionT Id ℚ
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.get?_diff : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Raw α β}
  [inst_2 : LawfulBEq α], m₁.WF → m₂.WF → ∀ {k : α}, (m₁ \ m₂).get? k = if k ∈ m₂ then none else m₁.get? k
-- Mathlib.Algebra.Group.Hom.Instances
/-- If `G` is an additive commutative group, then `M →+ G` is an additive commutative
group too.  -/
AddMonoidHom.instAddCommGroup : {M : Type uM} → {N : Type uN} → [inst : AddZeroClass M] → [inst_1 : AddCommGroup N] → AddCommGroup (M →+ N)
-- Mathlib.Topology.Order.LiminfLimsup
Prod.instBoundedLENhdsClass : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : TopologicalSpace α]
  [inst_3 : TopologicalSpace β] [BoundedLENhdsClass α] [BoundedLENhdsClass β], BoundedLENhdsClass (α × β)
-- Mathlib.Algebra.Category.MonCat.Adjunctions
MonCat.adjoinOne_map : ∀ {X Y : Semigrp} (f : X ⟶ Y), MonCat.adjoinOne.map f = MonCat.ofHom (WithOne.mapMulHom (Semigrp.Hom.hom f))
-- Mathlib.CategoryTheory.Bicategory.Kan.IsKan
/-- An absolute right Kan lift is a right Kan lift.  -/
CategoryTheory.Bicategory.RightLift.IsAbsKan.isKan : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : B} → {f : b ⟶ a} → {g : c ⟶ a} → {t : CategoryTheory.Bicategory.RightLift f g} → t.IsAbsKan → t.IsKan
-- Mathlib.Algebra.Ring.Action.Invariant
IsInvariantSubring.mk : ∀ {M : Type u_1} {R : Type u_2} [inst : Monoid M] [inst_1 : Ring R] [inst_2 : MulSemiringAction M R] {S : Subring R},
  (∀ (m : M) {x : R}, x ∈ S → m • x ∈ S) → IsInvariantSubring M S
-- Mathlib.Algebra.Order.Group.Opposite
MulOpposite.op_nonpos : ∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] {a : α}, MulOpposite.op a ≤ 0 ↔ a ≤ 0
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.Hom.appLE_map' : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {U : Y.Opens} {V V' : X.Opens}
  (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U) (i : V = V'),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.appLE f U V' ⋯)
      (X.presheaf.map (CategoryTheory.eqToHom i).op) =
    AlgebraicGeometry.Scheme.Hom.appLE f U V e
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
NumberField.InfinitePlace.mkComplex_coe : ∀ {K : Type u_1} [inst : Field K] (φ : { φ // ¬NumberField.ComplexEmbedding.IsReal φ }),
  ↑(NumberField.InfinitePlace.mkComplex φ) = NumberField.InfinitePlace.mk ↑φ
-- Mathlib.Topology.Hom.ContinuousEvalConst
ContinuousOn.coeFun : ∀ {F : Type u_1} {α : Type u_2} {X : Type u_3} {Z : Type u_4} [inst : FunLike F α X] [inst_1 : TopologicalSpace F]
  [inst_2 : TopologicalSpace X] [ContinuousEvalConst F α X] [inst_4 : TopologicalSpace Z] {f : Z → F} {s : Set Z},
  ContinuousOn f s → ∀ (x : α), ContinuousOn (fun x_1 => (f x_1) x) s
-- Mathlib.Order.SuccPred.Basic
Order.lt_succ_iff : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : SuccOrder α] {a b : α} [NoMaxOrder α], a < Order.succ b ↔ a ≤ b
-- Mathlib.CategoryTheory.Monoidal.Multifunctor
/-- The bifunctor `- ⊗ (F -)`.  -/
CategoryTheory.MonoidalCategory.curriedTensorInsertFunctor₂ : {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] →
        [CategoryTheory.MonoidalCategory D] →
          CategoryTheory.Functor C D → CategoryTheory.Functor D (CategoryTheory.Functor C D)
-- Mathlib.Data.Set.Card
Set.encard_lt_top_iff : ∀ {α : Type u_1} {s : Set α}, s.encard < ⊤ ↔ s.Finite
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.map_smul : ∀ {R₁ : Type u_1} [inst : Semiring R₁] {M₁ : Type u_4} [inst_1 : TopologicalSpace M₁] [inst_2 : AddCommMonoid M₁]
  {M₂ : Type u_5} [inst_3 : TopologicalSpace M₂] [inst_4 : AddCommMonoid M₂] [inst_5 : Module R₁ M₁]
  [inst_6 : Module R₁ M₂] (e : M₁ ≃L[R₁] M₂) (c : R₁) (x : M₁), e (c • x) = c • e x
-- Mathlib.Topology.Instances.AddCircle.Defs
AddCircle.nsmul_eq_zero_iff : ∀ {𝕜 : Type u_1} [inst : Field 𝕜] {p : 𝕜} [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [hp : Fact (0 < p)]
  {u : AddCircle p} {n : ℕ}, 0 < n → (n • u = 0 ↔ ∃ m < n, ↑(↑m / ↑n * p) = u)
-- Mathlib.Order.Hom.Lattice
/-- The underlying function of a `SupHom`.

Do not use this function directly. Instead use the coercion coming from the `FunLike`
instance.  -/
SupHom.toFun : {α : Type u_6} → {β : Type u_7} → [inst : Max α] → [inst_1 : Max β] → SupHom α β → α → β
-- Mathlib.RingTheory.SurjectiveOnStalks
RingHom.surjectiveOnStalks_iff_forall_ideal : ∀ {R : Type u_1} [inst : CommRing R] {S : Type u_2} [inst_1 : CommRing S] {f : R →+* S},
  f.SurjectiveOnStalks ↔ ∀ (I : Ideal S), I ≠ ⊤ → ∀ (s : S), ∃ x r, ∃ c ∉ I, f r ∉ I ∧ c * f r * s = c * f x
-- Mathlib.Probability.Kernel.MeasurableIntegral
MeasureTheory.StronglyMeasurable.integral_kernel_prod_left'' : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} {a : α} {E : Type u_4} [inst : NormedAddCommGroup E] {η : ProbabilityTheory.Kernel (α × β) γ}
  [ProbabilityTheory.IsSFiniteKernel η] [inst_2 : NormedSpace ℝ E] {f : γ × β → E},
  MeasureTheory.StronglyMeasurable f → MeasureTheory.StronglyMeasurable fun y => ∫ (x : γ), f (x, y) ∂η (a, y)
-- Mathlib.Topology.UniformSpace.CompactConvergence
/-- Any pair of a homeomorphism `X ≃ₜ Z` and an isomorphism `Y ≃ᵤ T` of uniform spaces gives rise
to an isomorphism `C(X, Y) ≃ᵤ C(Z, T)`.  -/
UniformEquiv.arrowCongr : {α : Type u₁} →
  {β : Type u₂} →
    [inst : TopologicalSpace α] →
      [inst_1 : UniformSpace β] →
        {γ : Type u_1} →
          {δ : Type u_2} →
            [inst_2 : TopologicalSpace γ] → [inst_3 : UniformSpace δ] → α ≃ₜ γ → β ≃ᵤ δ → C(α, β) ≃ᵤ C(γ, δ)
-- Mathlib.Algebra.Group.Subgroup.Ker
Subgroup.mk.congr_simp : ∀ {G : Type u_3} [inst : Group G] (toSubmonoid toSubmonoid_1 : Submonoid G)
  (e_toSubmonoid : toSubmonoid = toSubmonoid_1)
  (inv_mem' : ∀ {x : G}, x ∈ toSubmonoid.carrier → x⁻¹ ∈ toSubmonoid.carrier),
  { toSubmonoid := toSubmonoid, inv_mem' := inv_mem' } = { toSubmonoid := toSubmonoid_1, inv_mem' := ⋯ }
-- Init.Grind.Config
/-- Configuration for interactive mode.
We disable `clean := false`.
 -/
Lean.Grind.ConfigInteractive : Type
-- Mathlib.Algebra.Order.GroupWithZero.Finset
Finset.inf'_mul_le_mul_inf'_of_nonneg : ∀ {ι : Type u_1} {M₀ : Type u_2} [inst : MonoidWithZero M₀] {s : Finset ι} {a b : ι → M₀} [inst_1 : SemilatticeInf M₀]
  [PosMulMono M₀] [MulPosMono M₀],
  (∀ i ∈ s, 0 ≤ a i) → (∀ i ∈ s, 0 ≤ b i) → ∀ (hs : s.Nonempty), s.inf' hs a * s.inf' hs b ≤ s.inf' hs (a * b)
-- Init.Data.Float.Model.Float
Float.Model.instBEq : BEq Float.Model
-- Mathlib.Tactic.Linarith.Datatypes
/-- The description of the preprocessor.  -/
Mathlib.Tactic.Linarith.PreprocessorBase.description : Mathlib.Tactic.Linarith.PreprocessorBase → String
-- Mathlib.Logic.Equiv.Option
/-- **Alias** of `Equiv.removeNoneAux`.

---

If we have a value on one side of an `Equiv` of `Option`
we also have a value on the other side of the equivalence
 -/
Equiv.removeNone_aux : {α : Type u_1} → {β : Type u_2} → Option α ≃ Option β → α → β
-- Init.Data.SInt.Lemmas
Int32.toInt16_ofIntLE : ∀ {n : ℤ} (h₁ : Int32.minValue.toInt ≤ n) (h₂ : n ≤ Int32.maxValue.toInt),
  (Int32.ofIntLE n h₁ h₂).toInt16 = Int16.ofInt n
-- Lean.Parser.Term
/-- Manually prove that the termination measure (as specified with `termination_by` or inferred)
decreases at each recursive call.

By default, the tactic `decreasing_tactic` is used.

Forces the use of well-founded recursion and is hence incompatible with
`termination_by structural`.
 -/
Lean.Parser.Termination.decreasingBy : Lean.Parser.Parser
-- Mathlib.Data.Sum.Basic
Sum.update_inl_comp_inl : ∀ {α : Type u} {β : Type v} {γ : Type u_1} [inst : DecidableEq α] [inst_1 : DecidableEq (α ⊕ β)] {f : α ⊕ β → γ} {i : α}
  {x : γ}, Function.update f (Sum.inl i) x ∘ Sum.inl = Function.update (f ∘ Sum.inl) i x
-- Mathlib.Algebra.Order.Interval.Multiset
Multiset.map_add_right_Ioo : ∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [IsOrderedCancelAddMonoid α] [ExistsAddOfLE α]
  [inst_4 : LocallyFiniteOrder α] (a b c : α),
  Multiset.map (fun x => x + c) (Multiset.Ioo a b) = Multiset.Ioo (a + c) (b + c)
-- Mathlib.Algebra.Algebra.Opposite
/-- The canonical algebra isomorphism from `Aᵐᵒᵖ` to `Module.End A A` induced by the right
multiplication.  -/
AlgEquiv.moduleEndSelf : (R : Type u_1) →
  {A : Type u_3} → [inst : CommSemiring R] → [inst_1 : Semiring A] → [inst_2 : Algebra R A] → Aᵐᵒᵖ ≃ₐ[R] Module.End A A
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.image_div : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : DecidableEq α] [inst_1 : DecidableEq β] [inst_2 : Group α]
  [inst_3 : DivisionMonoid β] [inst_4 : FunLike F α β] [MonoidHomClass F α β] (f : F) {s t : Finset α},
  Finset.image (⇑f) (s / t) = Finset.image (⇑f) s / Finset.image (⇑f) t
-- Mathlib.Algebra.Algebra.NonUnitalHom
NonUnitalAlgHom.addHomMk_coe : ∀ {R : Type u} {S : Type u₁} [inst : Monoid R] [inst_1 : Monoid S] {φ : R →* S} {A : Type v} {B : Type w}
  [inst_2 : NonUnitalNonAssocSemiring A] [inst_3 : DistribMulAction R A] [inst_4 : NonUnitalNonAssocSemiring B]
  [inst_5 : DistribMulAction S B] (f : A →ₛₙₐ[φ] B), { toFun := ⇑f, map_add' := ⋯ } = ↑f
-- Mathlib.Algebra.Algebra.Operations
Submodule.smul_assoc : ∀ {R : Type u} [inst : Semiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Module R A] {M : Type u_1}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Module A M] [inst_6 : IsScalarTower R A M] {B : Type u_2}
  [inst_7 : Semiring B] [inst_8 : Module R B] [inst_9 : Module A B] [inst_10 : Module B M]
  [inst_11 : IsScalarTower R A B] [inst_12 : IsScalarTower R B M] [IsScalarTower A B M] (I : Submodule R A)
  (J : Submodule R B) (N : Submodule R M), (I • J) • N = I • J • N
-- Lean.Data.Lsp.Internal
Lean.Lsp.instForInIdDeclsProdStringDeclInfo : ForIn Id Lean.Lsp.Decls (String × Lean.Lsp.DeclInfo)
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.Λ'.copy.inj : ∀ {q q_1 : Turing.PartrecToTM2.Λ'}, q.copy = q_1.copy → q = q_1
-- Mathlib.Topology.VectorBundle.Basic
VectorBundleCore.toFiberBundleCore_coordChange : ∀ {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 ι),
  Z.toFiberBundleCore.coordChange = fun i j b => ⇑(Z.coordChange i j b)
-- Init.Grind.Module.NatModuleNorm
Lean.Grind.Linarith.Expr.denoteN.match_1.congr_eq_1 : ∀ (motive : Lean.Grind.Linarith.Expr → Sort u_1) (x : Lean.Grind.Linarith.Expr)
  (h_1 : (a b : Lean.Grind.Linarith.Expr) → motive (a.sub b)) (h_2 : (a : Lean.Grind.Linarith.Expr) → motive a.neg)
  (h_3 : (k : ℤ) → (a : Lean.Grind.Linarith.Expr) → motive (Lean.Grind.Linarith.Expr.intMul k a))
  (h_4 : Unit → motive Lean.Grind.Linarith.Expr.zero)
  (h_5 : (v : Lean.Grind.Linarith.Var) → motive (Lean.Grind.Linarith.Expr.var v))
  (h_6 : (a b : Lean.Grind.Linarith.Expr) → motive (a.add b))
  (h_7 : (k : ℕ) → (a : Lean.Grind.Linarith.Expr) → motive (Lean.Grind.Linarith.Expr.natMul k a))
  (a b : Lean.Grind.Linarith.Expr),
  x = a.sub b →
    (match x with
      | a.sub b => h_1 a b
      | a.neg => h_2 a
      | Lean.Grind.Linarith.Expr.intMul k a => h_3 k a
      | Lean.Grind.Linarith.Expr.zero => h_4 ()
      | Lean.Grind.Linarith.Expr.var v => h_5 v
      | a.add b => h_6 a b
      | Lean.Grind.Linarith.Expr.natMul k a => h_7 k a) ≍
      h_1 a b
-- Mathlib.Order.CompleteBooleanAlgebra
OrderDual.instCompleteAtomicBooleanAlgebra : {α : Type u} → [CompleteAtomicBooleanAlgebra α] → CompleteAtomicBooleanAlgebra αᵒᵈ
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
Finset.prod.eq_1 : ∀ {ι : Type u_1} {M : Type u_3} [inst : CommMonoid M] (s : Finset ι) (f : ι → M), s.prod f = (Multiset.map f s.val).prod
-- Mathlib.Topology.UniformSpace.Cauchy
/-- A Cauchy sequence in a complete space converges  -/
cauchySeq_tendsto_of_complete : ∀ {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [inst : Preorder β] [CompleteSpace α] {u : β → α},
  CauchySeq u → ∃ x, Filter.Tendsto u Filter.atTop (nhds x)
-- Batteries.Recycling.RBTree.Basic
/-- The first half of Okasaki's `balance`, concerning red-red sequences in the left child.  -/
RBTree.RBNode.balance1 : {α : Type u_1} → RBTree.RBNode α → α → RBTree.RBNode α → RBTree.RBNode α
-- Mathlib.Computability.TuringMachine.PostTuringMachine
/-- The set of accessible machine states, assuming that the input machine is supported on `S`,
are the normal states embedded from `S`, plus all write states accessible from these states.  -/
Turing.TM1to1.trSupp : {Γ : Type u_1} →
  {Λ : Type u_2} →
    {σ : Type u_3} → (Λ → Turing.TM1.Stmt Γ Λ σ) → [Fintype Γ] → Finset Λ → Finset (Turing.TM1to1.Λ' Γ Λ σ)
-- Mathlib.Algebra.Homology.Double
/-- Given a complex shape `c : ComplexShape ι` (with no loop), `X : C` and `j : ι`,
this is a quite explicit choice of corepresentative of the functor which sends
`K : HomologicalComplex C c` to `X ⟶ K.X j`.  -/
HomologicalComplex.evalCompCoyonedaCorepresentative : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      [CategoryTheory.Limits.HasZeroObject C] → {ι : Type u_2} → (c : ComplexShape ι) → C → ι → HomologicalComplex C c
-- Mathlib.Data.WSeq.Relation
Stream'.WSeq.LiftRel.symm : ∀ {α : Type u} (R : α → α → Prop) [Std.Symm R], Std.Symm (Stream'.WSeq.LiftRel R)
-- Mathlib.Algebra.Homology.HomotopyCategory.Plus
HomotopyCategory.instIsTriangulatedIntUpPlus : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.Limits.HasBinaryBiproducts C],
  (HomotopyCategory.plus C).IsTriangulated
-- Init.WF
Acc.ndrecOn : {α : Sort u2} →
  {r : α → α → Prop} →
    {C : α → Sort u1} →
      {a : α} → Acc r a → ((x : α) → (∀ (y : α), r y x → Acc r y) → ((y : α) → r y x → C y) → C x) → C a
-- Mathlib.CategoryTheory.Adjunction.Whiskering
CategoryTheory.Adjunction.whiskerLeft_unit_app_app : ∀ (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]
  {F : CategoryTheory.Functor D E} {G : CategoryTheory.Functor E D} (adj : F ⊣ G) (X : CategoryTheory.Functor D C)
  (X_1 : D), ((CategoryTheory.Adjunction.whiskerLeft C adj).unit.app X).app X_1 = X.map (adj.unit.app X_1)
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.Mor₂.of.injEq : ∀ (η η_1 : Mathlib.Tactic.BicategoryLike.Atom),
  (Mathlib.Tactic.BicategoryLike.Mor₂.of η = Mathlib.Tactic.BicategoryLike.Mor₂.of η_1) = (η = η_1)
-- Mathlib.CategoryTheory.Sites.Equivalence
CategoryTheory.Equivalence.sheafCongr.counitIso_hom_app_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] (K : CategoryTheory.GrothendieckTopology D) (e : C ≌ D) (A : Type u₃)
  [inst_2 : CategoryTheory.Category.{v₃, u₃} A] [inst_3 : CategoryTheory.Functor.IsDenseSubsite K J e.inverse]
  (X : CategoryTheory.Sheaf K A) (X_1 : Dᵒᵖ),
  ((CategoryTheory.Equivalence.sheafCongr.counitIso J K e A).hom.app X).hom.app X_1 =
    X.obj.map (e.counitIso.inv.app (Opposite.unop X_1)).op
-- Mathlib.CategoryTheory.Adjunction.Limits
CategoryTheory.Adjunction.conesIsoComponentInv.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) {J : Type u}
  [inst_2 : CategoryTheory.Category.{v, u} J] {K : CategoryTheory.Functor J D} (X : Cᵒᵖ)
  (t : ((CategoryTheory.cones J C).obj (K.comp G)).obj X),
  adj.conesIsoComponentInv X t =
    { app := fun j => (adj.homEquiv (Opposite.unop X) (K.obj j)).symm (t.app j), naturality := ⋯ }
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
MultipliableUniformlyOn.mono : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : CommMonoid α] {f : ι → β → α} {s : Set β}
  [inst_1 : UniformSpace α] {t : Set β}, MultipliableUniformlyOn f t → s ⊆ t → MultipliableUniformlyOn f s
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.ofArrows_mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {I : Type u_1} {X : C} (Y : I → C) (f : (i : I) → Y i ⟶ X)
  (i : I), (CategoryTheory.Sieve.ofArrows Y f).arrows (f i)
-- Mathlib.Data.Rat.Cast.Order
/-- Coercion from `ℚ` as an order embedding.  -/
Rat.castOrderEmbedding : {K : Type u_5} → [inst : Field K] → [inst_1 : LinearOrder K] → [IsStrictOrderedRing K] → ℚ ↪o K