mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Category.Cat
/-- Bicategory structure on `Cat`  -/
CategoryTheory.Cat.bicategory : CategoryTheory.Bicategory CategoryTheory.Cat
-- Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
/-- The tangent of an angle in a right-angled triangle as a ratio of sides, version subtracting
vectors.  -/
Orientation.tan_oangle_sub_left_of_oangle_eq_pi_div_two : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [hd2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y : V}, o.oangle x y = ↑(Real.pi / 2) → (o.oangle (x - y) x).tan = ‖y‖ / ‖x‖
-- Mathlib.Data.Set.Image
Option.range_eq : ∀ {α : Type u_1} {β : Type u_2} (f : Option α → β), Set.range f = insert (f none) (Set.range (f ∘ some))
-- Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation
LeftInvariantDerivation.lift_smul : ∀ {𝕜 : 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} {G : Type u_4}
  [inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : Monoid G] [inst_7 : ContMDiffMul I (↑⊤) G]
  (X : LeftInvariantDerivation I G) (k : 𝕜), ↑(k • X) = k • ↑X
-- Init.Data.BitVec.Bitblast
BitVec.getElem_mul : ∀ {w : ℕ} {x y : BitVec w} {i : ℕ} (h : i < w), (x * y)[i] = (x.mulRec y w)[i]
-- Mathlib.Algebra.Category.BialgCat.Monoidal
BialgCat.tensorUnit_def : ∀ (R : Type u) [inst : CommRing R], CategoryTheory.MonoidalCategoryStruct.tensorUnit (BialgCat R) = BialgCat.of R R
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.eval₂_zero : ∀ {R : Type u} {S₁ : Type v} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁] (f : R →+* S₁)
  (g : σ → S₁), MvPolynomial.eval₂ f g 0 = 0
-- Init.Data.List.MinMaxOn
_private.Init.Data.List.MinMaxOn.0.List.minOn?.eq_2 : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] (f : α → β) (x : α) (xs : List α),
  List.minOn? f (x :: xs) = some (List.foldl (minOn f) x xs)
-- Lean.Data.Lsp.Window
Lean.Lsp.MessageType.info.sizeOf_spec : sizeOf Lean.Lsp.MessageType.info = 1
-- Mathlib.MeasureTheory.Measure.HasOuterApproxClosed
IsClosed.apprSeq.congr_simp : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : HasOuterApproxClosed X] {F F_1 : Set X} (e_F : F = F_1)
  (hF : IsClosed F) (a a_1 : ℕ), a = a_1 → hF.apprSeq a = ⋯.apprSeq a_1
-- Lean.Meta.Tactic.Grind.EMatch
Lean.Meta.Grind.EMatch.instInhabitedChoice : Inhabited Lean.Meta.Grind.EMatch.Choice
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
/-- The orthogonal projection onto `K` of an element of `Kᗮ` is zero.  -/
Submodule.orthogonalProjectionOnto_apply_of_mem_orthogonal : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {K : Submodule 𝕜 E} [inst_3 : K.HasOrthogonalProjection] {v : E}, v ∈ Kᗮ → K.orthogonalProjectionOnto v = 0
-- Mathlib.Probability.Moments.SubGaussian
/-- **Azuma-Hoeffding inequality** for sub-Gaussian random variables.  -/
ProbabilityTheory.measure_sum_ge_le_of_hasCondSubgaussianMGF : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [inst : StandardBorelSpace Ω] {Y : ℕ → Ω → ℝ}
  {cY : ℕ → NNReal} {ℱ : MeasureTheory.Filtration ℕ mΩ} [inst_1 : MeasureTheory.IsZeroOrProbabilityMeasure μ],
  MeasureTheory.StronglyAdapted ℱ Y →
    ProbabilityTheory.HasSubgaussianMGF (Y 0) (cY 0) μ →
      ∀ (n : ℕ),
        (∀ i < n - 1, ProbabilityTheory.HasCondSubgaussianMGF (↑ℱ i) ⋯ (Y (i + 1)) (cY (i + 1)) μ) →
          ∀ {ε : ℝ},
            0 ≤ ε →
              μ.real {ω | ε ≤ ∑ i ∈ Finset.range n, Y i ω} ≤ Real.exp (-ε ^ 2 / (2 * ↑(∑ i ∈ Finset.range n, cY i)))
-- Mathlib.Logic.Function.Basic
Function.extend_injective : ∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β},
  Function.Injective f → ∀ (e' : β → γ), Function.Injective fun g => Function.extend f g e'
-- Mathlib.CategoryTheory.Groupoid
CategoryTheory.Groupoid.isoEquivHom_apply : ∀ {C : Type u} [inst : CategoryTheory.Groupoid C] (X Y : C) (self : X ≅ Y),
  (CategoryTheory.Groupoid.isoEquivHom X Y) self = self.hom
-- Mathlib.MeasureTheory.SetSemiring
/-- **Alias** of `MeasureTheory.IsSetSemiring.sdiff_sUnion_eq_sUnion_disjointOfDiffUnion`. -/
MeasureTheory.IsSetSemiring.diff_sUnion_eq_sUnion_disjointOfDiffUnion : ∀ {α : Type u_1} {C : Set (Set α)} {s : Set α} {I : Finset (Set α)} (hC : MeasureTheory.IsSetSemiring C) (hs : s ∈ C)
  (hI : ↑I ⊆ C), s \ ⋃₀ ↑I = ⋃₀ ↑(hC.disjointOfDiffUnion hs hI)
-- Mathlib.Data.Real.Basic
Real.ext_cauchy_iff : ∀ {x y : ℝ}, x = y ↔ x.cauchy = y.cauchy
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.aleph0_le_lift : ∀ {c : Cardinal.{u}}, Cardinal.aleph0 ≤ Cardinal.lift.{v, u} c ↔ Cardinal.aleph0 ≤ c
-- Mathlib.CategoryTheory.Comma.Over.Pullback
CategoryTheory.Over.forgetMapTerminal_hom_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : C) {T : C} (hT : CategoryTheory.Limits.IsTerminal T)
  (X_1 : CategoryTheory.Over X),
  (CategoryTheory.Over.forgetMapTerminal X hT).hom.app X_1 = CategoryTheory.CategoryStruct.id X_1.left
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.contains_keysArray : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α}, m.keysArray.contains k = m.contains k
-- Mathlib.CategoryTheory.Iso
CategoryTheory.Iso.trans_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (α : X ≅ Y) (β : Y ≅ Z),
  (α ≪≫ β).hom = CategoryTheory.CategoryStruct.comp α.hom β.hom
-- Mathlib.Order.Filter.AtTopBot.Basic
Filter.tendsto_comp_val_Iic_atBot : ∀ {α : Type u_3} {β : Type u_4} [inst : Preorder α] [IsCodirectedOrder α] {a : α} {f : α → β} {l : Filter β},
  Filter.Tendsto (fun x => f ↑x) Filter.atBot l ↔ Filter.Tendsto f Filter.atBot l
-- Lean.Environment
Lean.PersistentEnvExtensionDescrCore.mk.sizeOf_spec : ∀ {α β σ : Type} [inst : SizeOf α] [inst_1 : SizeOf β] [inst_2 : SizeOf σ]
  (name : autoParam Lean.Name Lean.PersistentEnvExtensionDescrCore.name._autoParam) (mkInitial : IO σ)
  (addImportedFn : Array (Array α) → Lean.ImportM σ) (addEntryFn : σ → β → σ)
  (exportEntriesFnEx : Lean.Environment → σ → Lean.OLeanEntries (Array α)) (statsFn : σ → Std.Format)
  (asyncMode : Lean.EnvExtension.AsyncMode) (replay? : Option (Lean.ReplayFn σ)),
  sizeOf
      { name := name, mkInitial := mkInitial, addImportedFn := addImportedFn, addEntryFn := addEntryFn,
        exportEntriesFnEx := exportEntriesFnEx, statsFn := statsFn, asyncMode := asyncMode, replay? := replay? } =
    1 + sizeOf name + sizeOf asyncMode + sizeOf replay?
-- Std.Data.DTreeMap.Internal.WF.Defs
Std.DTreeMap.Internal.Impl.WF.below.filter : ∀ {α : Type u} [inst : Ord α] {motive : {β : α → Type v} → (a : Std.DTreeMap.Internal.Impl α β) → a.WF → Prop}
  {x : α → Type v} {t : Std.DTreeMap.Internal.Impl α x} {h : t.Balanced} {f : (a : α) → x a → Bool} (a : t.WF),
  Std.DTreeMap.Internal.Impl.WF.below a → motive t a → Std.DTreeMap.Internal.Impl.WF.below ⋯
-- Mathlib.CategoryTheory.Monoidal.Skeleton
CategoryTheory.instMonoidalSkeletonInverseSkeletonEquivalence : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] → (CategoryTheory.skeletonEquivalence C).inverse.Monoidal
-- Mathlib.LinearAlgebra.AffineSpace.Midpoint
midpoint_self_neg : ∀ (R : Type u_1) {V : Type u_2} [inst : Ring R] [inst_1 : Invertible 2] [inst_2 : AddCommGroup V] [inst_3 : Module R V]
  (x : V), midpoint R x (-x) = 0
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.fromEdgeSet_mono : ∀ {V : Type u} {s t : Set (Sym2 V)}, s ⊆ t → SimpleGraph.fromEdgeSet s ≤ SimpleGraph.fromEdgeSet t
-- Init.Meta.Defs
/-- Whenever `((a - b : Nat) : Int)` is found, register the disjunction
`b ≤ a ∧ ((a - b : Nat) : Int) = a - b ∨ a < b ∧ ((a - b : Nat) : Int) = 0`
for later splitting.
 -/
Lean.Meta.Omega.OmegaConfig.splitNatSub : Lean.Meta.Omega.OmegaConfig → Bool
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
/-- We say that `F` preserves (small) limits if it sends small
limit cones over any diagram to limit cones.  -/
CategoryTheory.Limits.PreservesLimits : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} → [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → CategoryTheory.Functor C D → Prop
-- Mathlib.Topology.UniformSpace.Basic
mem_entourageProd : ∀ {α : Type ua} {β : Type ub} {u : SetRel α α} {v : SetRel β β} {p : (α × β) × α × β},
  p ∈ entourageProd u v ↔ (p.1.1, p.2.1) ∈ u ∧ (p.1.2, p.2.2) ∈ v
-- Mathlib.AlgebraicGeometry.Modules.Tilde
/-- **Alias** of `AlgebraicGeometry.Scheme.Modules.restrictAppIso_smul_Spec`. -/
AlgebraicGeometry.Scheme.Modules.Scheme.Modules.restrictAppIso_smul_Spec : ∀ {R : CommRingCat} {M : (AlgebraicGeometry.Spec R).Modules} {S : CommRingCat} (f : R ⟶ S)
  [inst : AlgebraicGeometry.IsOpenImmersion (AlgebraicGeometry.Spec.map f)] {U : (AlgebraicGeometry.Spec S).Opens}
  (r : ↑R) (x : ↑((M.restrict (AlgebraicGeometry.Spec.map f)).presheaf.obj (Opposite.op U))),
  (CategoryTheory.ConcreteCategory.hom
        (AlgebraicGeometry.Scheme.Modules.restrictAppIso (AlgebraicGeometry.Spec.map f) M U).hom)
      ((CategoryTheory.ConcreteCategory.hom f) r • x) =
    r •
      (CategoryTheory.ConcreteCategory.hom
          (AlgebraicGeometry.Scheme.Modules.restrictAppIso (AlgebraicGeometry.Spec.map f) M U).hom)
        x
-- Mathlib.Tactic.Determinant.Bird.Cert
Mathlib.Tactic.Determinant.CertCache.mk.sizeOf_spec : ∀ {u : Lean.Level} {α : Q(Type u)} {rα : Q(CommRing «$α»)}
  (entryCache : Std.HashMap (ℕ × ℕ) (Mathlib.Tactic.Determinant.Cert rα))
  (iterStepEntryCache : Std.HashMap (ℕ × ℕ × ℕ) (Mathlib.Tactic.Determinant.Cert rα))
  (diagCache : Std.HashMap (ℕ × ℕ) (Mathlib.Tactic.Determinant.Cert rα)),
  sizeOf { entryCache := entryCache, iterStepEntryCache := iterStepEntryCache, diagCache := diagCache } =
    1 + sizeOf entryCache + sizeOf iterStepEntryCache + sizeOf diagCache
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.coeff_zero_X : ∀ {R : Type u_1} [inst : Semiring R], (PowerSeries.coeff 0) PowerSeries.X = 0
-- Mathlib.ModelTheory.Types
FirstOrder.Language.Theory.CompleteType.nonempty_iff : ∀ {L : FirstOrder.Language} {T : L.Theory} {α : Type w}, Nonempty (T.CompleteType α) ↔ T.IsSatisfiable
-- Mathlib.RingTheory.AdicCompletion.Functoriality
AdicCompletion.map_ext''_iff : ∀ {R : Type u_1} [inst : CommRing R] {I : Ideal R} {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {N : Type u_3} [inst_3 : AddCommGroup N] [inst_4 : Module R N] {f g : AdicCompletion I M →ₗ[R] N},
  f = g ↔ f ∘ₗ AdicCompletion.mk I M = g ∘ₗ AdicCompletion.mk I M
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.pow_vle_pow_of_one_vle : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : ValuativeRel R] {a : R}, 1 ≤ᵥ a → ∀ {n m : ℕ}, n ≤ m → a ^ n ≤ᵥ a ^ m
-- Lean.Parser.Term
Lean.Parser.Term.trueVal.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Analysis.ODE.Basic
IsIntegralCurveAt.eq_1 : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (γ : ℝ → E) (v : ℝ → E → E) (t₀ : ℝ),
  IsIntegralCurveAt γ v t₀ = ∀ᶠ (t : ℝ) in nhds t₀, HasDerivAt γ (v t (γ t)) t
-- Init.Omega.Int
Lean.Omega.Int.not_le_of_lt : ∀ {x y : ℤ}, y < x → ¬x ≤ y
-- Mathlib.GroupTheory.Nilpotent
/-- Products of nilpotent groups are nilpotent.  -/
AddGroup.isNilpotent_sum : ∀ {G₁ : Type u_2} {G₂ : Type u_3} [inst : AddGroup G₁] [inst_1 : AddGroup G₂] [AddGroup.IsNilpotent G₁]
  [AddGroup.IsNilpotent G₂], AddGroup.IsNilpotent (G₁ × G₂)
-- Mathlib.Topology.Connected.Basic
IsConnected.preimage_of_isOpenMap : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {s : Set β},
  IsConnected s → ∀ {f : α → β}, Function.Injective f → IsOpenMap f → s ⊆ Set.range f → IsConnected (f ⁻¹' s)
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithInitial.false_of_to_star : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C}
  (f : CategoryTheory.WithInitial.of X ⟶ CategoryTheory.WithInitial.star), False
-- Mathlib.CategoryTheory.Limits.Final
CategoryTheory.Functor.Final.colimitCoconeOfComp_cocone : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [inst_2 : F.Final] {E : Type u₃} [inst_3 : CategoryTheory.Category.{v₃, u₃} E]
  {G : CategoryTheory.Functor D E} (t : CategoryTheory.Limits.ColimitCocone (F.comp G)),
  (CategoryTheory.Functor.Final.colimitCoconeOfComp F t).cocone = CategoryTheory.Functor.Final.extendCocone.obj t.cocone
-- Aesop.RuleSet
/-- A global Aesop rule set. When we tag a declaration with `@[aesop]`, it is stored
in one or more of these rule sets. Internally, a `GlobalRuleSet` is composed of
a `BaseRuleSet` (stored in an Aesop rule set extension) plus a set of simp
theorems (stored in a `SimpExtension`).
 -/
Aesop.GlobalRuleSet : Type
-- Init.Data.Array.Find
_private.Init.Data.Array.Find.0.List.of_findIdx?_eq_some.match_1.splitter : {α : Type u_1} →
  (motive : Option α → Sort u_2) → (x : Option α) → ((a : α) → motive (some a)) → (Unit → motive none) → motive x
-- Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct
CategoryTheory.Limits.instIsIPCOfShapeFunctorOfHasFilteredColimitsOfSize : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (ι : Type u_1)
  [inst_1 : CategoryTheory.Limits.HasProductsOfShape ι C] [CategoryTheory.Limits.IsIPCOfShape.{w, u_1, v, u} ι C]
  [CategoryTheory.Limits.HasFilteredColimitsOfSize.{w, w, v, u} C] {D : Type u₁}
  [inst_4 : CategoryTheory.Category.{v₁, u₁} D],
  CategoryTheory.Limits.IsIPCOfShape.{w, u_1, max u₁ v, max (max (max u u₁) v) v₁} ι (CategoryTheory.Functor D C)
-- Mathlib.CategoryTheory.Monoidal.Free.Coherence
/-- We say an object in the free monoidal category is in normal form if it is of the form
`(((𝟙_ C) ⊗ X₁) ⊗ X₂) ⊗ ⋯`.  -/
CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject : Type u → Type u
-- Mathlib.Topology.Sheaves.EtaleSpace
/-- If `s` is a section of a presheaf `F` over `U` with germ at `g.base` equal to `g.germ`,
then a neighborhood of `g` consists of germs of `s` at points `x ∈ U`.  -/
TopCat.Presheaf.EtaleSpace.eventually_nhds : ∀ {X : TopCat} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {CC : C → Type v} {FC : C → C → Type w}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC]
  [inst_3 : CategoryTheory.Limits.HasColimits C] {F : TopCat.Presheaf C X} (g : F.EtaleSpace)
  {U : TopologicalSpace.Opens ↑X} (h : g.base ∈ U) (s : CategoryTheory.ToType (F.obj (Opposite.op U))),
  (CategoryTheory.ConcreteCategory.hom (F.germ U g.base h)) s = g.germ →
    ∀ᶠ (g' : F.EtaleSpace) in nhds g,
      ∃ (hgU : g'.base ∈ U), g'.germ = (CategoryTheory.ConcreteCategory.hom (F.germ U g'.base hgU)) s
-- Lean.PrettyPrinter
Lean.PrettyPrinter.ppTerm : Lean.Term → Lean.CoreM Std.Format
-- Mathlib.SetTheory.Lists
Lists'.instHasSubsetTrue : {α : Type u_1} → HasSubset (Lists' α true)
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalAlgebra.sInf_toSubmodule : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] [inst_4 : SMulCommClass R A A] (S : Set (NonUnitalSubalgebra R A)),
  (sInf S).toSubmodule = sInf (NonUnitalSubalgebra.toSubmodule '' S)
-- Init.Data.List.Basic
/-- Pads `l : List α` on the right with repeated occurrences of `a : α` until it is of length `n`. If
`l` already has at least `n` elements, it is returned unmodified.

Examples:
 * `[1, 2, 3].rightpad 5 0 = [1, 2, 3, 0, 0]`
 * `["red", "green", "blue"].rightpad 4 "blank" = ["red", "green", "blue", "blank"]`
 * `["red", "green", "blue"].rightpad 3 "blank" = ["red", "green", "blue"]`
 * `["red", "green", "blue"].rightpad 1 "blank" = ["red", "green", "blue"]`
 -/
List.rightpad : {α : Type u} → ℕ → α → List α → List α
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.fullSubcategory_tensorUnit_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {P : CategoryTheory.ObjectProperty C} [inst_2 : P.IsClosedUnderLimitsOfShape (CategoryTheory.Discrete PEmpty.{1})]
  [inst_3 : P.IsClosedUnderLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair)],
  (CategoryTheory.MonoidalCategoryStruct.tensorUnit P.FullSubcategory).obj =
    CategoryTheory.MonoidalCategoryStruct.tensorUnit C
-- Mathlib.RingTheory.Noetherian.OfPrime
/-- If all non-zero prime ideals in a commutative ring are finitely generated,
so are all other ideals.  -/
IsNoetherianRing.of_prime_ne_bot : ∀ {R : Type u_1} [inst : CommRing R], (∀ (I : Ideal R), I.IsPrime → I ≠ ⊥ → I.FG) → IsNoetherianRing R
-- Mathlib.Data.Part
Part.map_bind : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_4} (f : α → Part β) (x : Part α) (g : β → γ),
  Part.map g (x.bind f) = x.bind fun y => Part.map g (f y)
-- Mathlib.Algebra.Group.Action.Faithful
faithfulSMul_iff_injective_smul_one : ∀ (R : Type u_4) (A : Type u_5) [inst : MulOneClass A] [inst_1 : SMul R A] [IsScalarTower R A A],
  FaithfulSMul R A ↔ Function.Injective fun r => r • 1
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
ContinuousOn.intervalIntegrable : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsLocallyFiniteMeasure μ]
  {u : ℝ → E} {a b : ℝ}, ContinuousOn u (Set.uIcc a b) → IntervalIntegrable u μ a b
-- Lean.Meta.Tactic.Try.Collect
Lean.Meta.Try.Collector.OrdSet.mk.injEq : ∀ {α : Type} [inst : Hashable α] [inst_1 : BEq α] (elems : Array α) (set : Std.HashSet α) (elems_1 : Array α)
  (set_1 : Std.HashSet α),
  ({ elems := elems, set := set } = { elems := elems_1, set := set_1 }) = (elems = elems_1 ∧ set = set_1)
-- Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
AddSubgroup.op_bot : ∀ {G : Type u_2} [inst : AddGroup G], ⊥.op = ⊥
-- Mathlib.FieldTheory.Galois.NormalBasis
/-- Given a finite Galois extension `L/K`, `normalBasis K L` is a basis of `L` over `K`
that is an orbit under the Galois group action.  -/
IsGalois.normalBasis : (K : Type u_1) →
  (L : Type u_2) →
    [inst : Field K] →
      [inst_1 : Field L] → [inst_2 : Algebra K L] → [FiniteDimensional K L] → [IsGalois K L] → Module.Basis Gal(L/K) K L
-- Mathlib.Data.PFun
PFun.image_def : ∀ {α : Type u_1} {β : Type u_2} (f : α →. β) (s : Set α), f.image s = {y | ∃ x ∈ s, y ∈ f x}
-- Batteries.Data.Array.Scan
List.toArray_scanrM : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {init : β} [inst : Monad m] [LawfulMonad m] {f : α → β → m β}
  {as : List α}, List.toArray <$> List.scanrM f init as = Array.scanrM f init as.toArray
-- Mathlib.Algebra.Lie.Rank
LieModule.rank_le_natTrailingDegree_charpoly_ad : ∀ (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 : Module.Finite R L] [inst_4 : Module.Free R L] [inst_5 : AddCommGroup M] [inst_6 : Module R M]
  [inst_7 : LieRingModule L M] [inst_8 : LieModule R L M] [inst_9 : Module.Finite R M] [inst_10 : Module.Free R M]
  (x : L) [Nontrivial R], LieModule.rank R L M ≤ (LinearMap.charpoly ((LieModule.toEnd R L M) x)).natTrailingDegree
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.isEmpty_toArray : ∀ {α : Type u} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β},
  (Std.DTreeMap.Internal.Impl.Const.toArray t).isEmpty = t.isEmpty
-- Std.Data.Iterators.Lemmas.Producers.Monadic.Vector
Std.Iterators.Vector.isPlausibleStep_iterFromIdxM_of_lt : ∀ {m : Type w → Type w'} [inst : Monad m] {β : Type w} {n : ℕ} {xs : Vector β n} {pos : ℕ} (h : pos < n),
  (xs.iterFromIdxM m pos).IsPlausibleStep (Std.IterStep.yield (xs.iterFromIdxM m (pos + 1)) xs[pos])
-- Mathlib.NumberTheory.MulChar.Basic
/-- The trivial multiplicative character. It takes the value `0` on non-units and
the value `1` on units.  -/
MulChar.trivial : (R : Type u_1) → [inst : CommMonoid R] → (R' : Type u_2) → [inst_1 : CommMonoidWithZero R'] → MulChar R R'
-- Mathlib.CategoryTheory.Bicategory.Modification.Lax
CategoryTheory.Lax.LaxTrans.Modification.mk.sizeOf_spec : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.LaxFunctor B C} {η θ : F ⟶ G} [inst_2 : SizeOf B] [inst_3 : SizeOf C]
  (app : (a : B) → η.app a ⟶ θ.app a)
  (naturality :
    autoParam
      (∀ {a b : B} (f : a ⟶ b),
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (app a) (G.map f)) (θ.naturality f) =
          CategoryTheory.CategoryStruct.comp (η.naturality f) (CategoryTheory.Bicategory.whiskerLeft (F.map f) (app b)))
      CategoryTheory.Lax.LaxTrans.Modification.naturality._autoParam),
  sizeOf { app := app, naturality := naturality } = 1
-- Mathlib.NumberTheory.TsumDivisorsAntidiagonal
/-- The map from `Nat.divisorsAntidiagonal n` to `ℕ+ × ℕ+` given by sending `n = a * b`
to `(a, b)`.  -/
divisorsAntidiagonalFactors : (n : ℕ+) → ↥(↑n).divisorsAntidiagonal → ℕ+ × ℕ+
-- Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup
spinGroup.val_toUnits_apply : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} (x : ↥(spinGroup Q)), ↑(spinGroup.toUnits x) = ↑x
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
/-- The range of a non-unital ring homomorphism is a non-unital subsemiring.
See note [range copy pattern].  -/
NonUnitalRingHom.srange : {R : Type u} →
  {S : Type v} →
    [inst : NonUnitalNonAssocSemiring R] →
      [inst_1 : NonUnitalNonAssocSemiring S] →
        {F : Type u_1} → [inst_2 : FunLike F R S] → [NonUnitalRingHomClass F R S] → F → NonUnitalSubsemiring S
-- Mathlib.RingTheory.Ideal.Height
/-- If `R` has finite Krull dimension, there exists a maximal ideal `m` with `ht m = dim R`.  -/
Ideal.exists_isMaximal_height : ∀ {R : Type u_1} [inst : CommRing R] [FiniteRingKrullDim R], ∃ p, p.IsMaximal ∧ ↑p.height = ringKrullDim R
-- Mathlib.Analysis.SpecificLimits.Normed
geom_series_mul_one_add : ∀ {R : Type u_4} [inst : NormedRing R] [HasSummableGeomSeries R] (x : R),
  ‖x‖ < 1 → (1 + x) * ∑' (i : ℕ), x ^ i = 2 * ∑' (i : ℕ), x ^ i - 1
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.basisFun_equivFun : ∀ (p : ENNReal) (𝕜 : Type u_1) (ι : Type u_2) [inst : Finite ι] [inst_1 : Ring 𝕜],
  (PiLp.basisFun p 𝕜 ι).equivFun = WithLp.linearEquiv p 𝕜 (ι → 𝕜)
-- Mathlib.Analysis.BoxIntegral.Partition.Filter
BoxIntegral.IntegrationParams.toFilteriUnion_congr : ∀ {ι : Type u_1} [inst : Fintype ι] (I : BoxIntegral.Box ι) (l : BoxIntegral.IntegrationParams)
  {π₁ π₂ : BoxIntegral.Prepartition I},
  π₁.iUnion = π₂.iUnion →
    BoxIntegral.IntegrationParams.toFilteriUnion I π₁ = BoxIntegral.IntegrationParams.toFilteriUnion I π₂
-- Mathlib.RingTheory.TensorProduct.Maps
Algebra.TensorProduct.lmul'_apply_tmul : ∀ {R : Type uR} {S : Type uS} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (a b : S),
  (Algebra.TensorProduct.lmul' R) (a ⊗ₜ[R] b) = a * b
-- Init.Data.Range.Polymorphic.Lemmas
_private.Init.Data.Range.Polymorphic.Lemmas.0.Std.Roo.Internal.toArray_eq_toArray_iter : ∀ {α : Type u} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.Rxo.IsAlwaysFinite α] [inst_4 : Std.PRange.LawfulUpwardEnumerable α] {r : Std.Roo α},
  r.toArray = (Std.Roo.Internal.iter r).toArray
-- Mathlib.MeasureTheory.SetAlgebra
/-- An algebra of sets is a ring of sets.  -/
MeasureTheory.IsSetAlgebra.isSetRing : ∀ {α : Type u_1} {𝒜 : Set (Set α)}, MeasureTheory.IsSetAlgebra 𝒜 → MeasureTheory.IsSetRing 𝒜
-- Mathlib.ModelTheory.Substructures
/-- The `L.Substructure` generated by a set.  -/
FirstOrder.Language.Substructure.closure : (L : FirstOrder.Language) → {M : Type w} → [inst : L.Structure M] → LowerAdjoint SetLike.coe