mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Probability.Kernel.Composition.MeasureCompProd
MeasureTheory.Measure.compProd_apply_prod : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α}
  {κ : ProbabilityTheory.Kernel α β} [MeasureTheory.SFinite μ] [ProbabilityTheory.IsSFiniteKernel κ] {s : Set α}
  {t : Set β}, MeasurableSet s → MeasurableSet t → (μ.compProd κ) (s ×ˢ t) = ∫⁻ (a : α) in s, (κ a) t ∂μ
-- Mathlib.RingTheory.AlgebraicIndependent.Transcendental
/-- If `A/R` is algebraic, then all algebraically independent families are empty.  -/
AlgebraicIndependent.isEmpty_of_isAlgebraic : ∀ {ι : Type u_1} {R : Type u_3} {A : Type v} {x : ι → A} [inst : CommRing R] [inst_1 : CommRing A]
  [inst_2 : Algebra R A], AlgebraicIndependent R x → ∀ [Algebra.IsAlgebraic R A], IsEmpty ι
-- Mathlib.Algebra.Module.Equiv.Basic
LinearMap.mk.congr_simp : ∀ {R : Type u_14} {S : Type u_15} [inst : Semiring R] [inst_1 : Semiring S] {σ : R →+* S} {M : Type u_16}
  {M₂ : Type u_17} [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module S M₂]
  (toAddHom toAddHom_1 : M →ₙ+ M₂) (e_toAddHom : toAddHom = toAddHom_1)
  (map_smul' : ∀ (m : R) (x : M), toAddHom.toFun (m • x) = σ m • toAddHom.toFun x),
  { toAddHom := toAddHom, map_smul' := map_smul' } = { toAddHom := toAddHom_1, map_smul' := ⋯ }
-- Mathlib.CategoryTheory.Adjunction.Basic
/-- The isomorphism which an adjunction `F ⊣ G` induces on `F.op ⋙ coyoneda`. This states that
`Adjunction.homEquiv` is natural in both arguments.  -/
CategoryTheory.Adjunction.compCoyonedaIso : {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} →
            (F ⊣ G) →
              (F.op.comp CategoryTheory.coyoneda ≅
                CategoryTheory.coyoneda.comp ((CategoryTheory.Functor.whiskeringLeft D C (Type v₁)).obj G))
-- Batteries.Data.Fin.Coding
Fin.encodeFun.eq_def : ∀ {n : ℕ} (x : ℕ) (x_1 : Fin x → Fin n),
  Fin.encodeFun x_1 =
    match x, x_1 with
    | 0, x => ⟨0, ⋯⟩
    | m.succ, f => ⟨n * ↑(Fin.encodeFun fun k => f k.succ) + ↑(f 0), ⋯⟩
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.Context.ctx : Lean.Elab.Tactic.Grind.Context → Lean.Meta.Grind.Context
-- Mathlib.CategoryTheory.Sites.Over
CategoryTheory.GrothendieckTopology.instIsContinuousOverStarOver : ∀ {C : Type u'} [inst : CategoryTheory.Category.{v_1, u'} C] [inst_1 : CategoryTheory.Limits.HasBinaryProducts C]
  {J : CategoryTheory.GrothendieckTopology C} (X : C), (CategoryTheory.Over.star X).IsContinuous J (J.over X)
-- Mathlib.RepresentationTheory.Intertwining
Representation.IntertwiningMap.comp_apply : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [inst : Semiring A] [inst_1 : Monoid G]
  [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid W] [inst_4 : AddCommMonoid U] [inst_5 : Module A V]
  [inst_6 : Module A W] [inst_7 : Module A U] (ρ : Representation A G V) (σ : Representation A G W)
  (τ : Representation A G U) (f : σ.IntertwiningMap τ) (g : ρ.IntertwiningMap σ) (v : V), (f.comp g) v = f (g v)
-- Mathlib.Data.Matrix.Mul
Matrix.natCast_mulVec : ∀ {m : Type u_2} {α : Type v} [inst : NonAssocSemiring α] [inst_1 : Fintype m] [inst_2 : DecidableEq m] (x : ℕ)
  (v : m → α), (↑x).mulVec v = ↑x • v
-- Mathlib.Topology.Compactness.Compact
ULift.compactSpace : ∀ {X : Type u} [inst : TopologicalSpace X] [CompactSpace X], CompactSpace (ULift.{v, u} X)
-- Mathlib.Order.SuccPred.Limit
/-- A successor limit is a value that isn't minimal and doesn't cover any other.

It's so named because in a successor order, a successor limit can't be the successor of anything
smaller.

Use `IsSuccPrelimit` if you want to include the case of a minimal element.  -/
Order.IsSuccLimit : {α : Type u_1} → [Preorder α] → α → Prop
-- Mathlib.Topology.Filter
Filter.Tendsto.nhds : ∀ {α : Type u_2} {X : Type u_4} [inst : TopologicalSpace X] {f : α → X} {l : Filter α} {x : X},
  Filter.Tendsto f l (nhds x) → Filter.Tendsto (nhds ∘ f) l (nhds (nhds x))
-- Mathlib.Topology.Order.LocalExtr
/-- `IsLocalExtr f s a` means `IsLocalMin f s a ∨ IsLocalMax f s a`.  -/
IsLocalExtr : {α : Type u} → {β : Type v} → [TopologicalSpace α] → [Preorder β] → (α → β) → α → Prop
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.toFinsupp_injective : ∀ {R : Type u} [inst : Semiring R], Function.Injective Polynomial.toFinsupp
-- Mathlib.RingTheory.Algebraic.Integral
instIsAlgebraicSubtypeMemSubalgebraAlgebraicClosure : ∀ (R : Type u_1) (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [inst_3 : IsDomain R],
  Algebra.IsAlgebraic R ↥(Subalgebra.algebraicClosure R S)
-- Mathlib.LinearAlgebra.PiTensorProduct.Dual
PiTensorProduct.dualDistribInvOfBasis.congr_simp : ∀ {ι : Type u_1} {R : Type u_2} {κ : ι → Type u_3} {M : ι → Type u_4} [inst : CommRing R]
  [inst_1 : (i : ι) → AddCommGroup (M i)] [inst_2 : (i : ι) → Module R (M i)] [inst_3 : Finite ι]
  [inst_4 : ∀ (i : ι), Finite (κ i)] (b b_1 : (i : ι) → Module.Basis (κ i) R (M i)),
  b = b_1 → PiTensorProduct.dualDistribInvOfBasis b = PiTensorProduct.dualDistribInvOfBasis b_1
-- Mathlib.NumberTheory.LSeries.Convergence
/-- If `f` and `g` agree on large `n : ℕ`, then their `LSeries` have the same
abscissa of absolute convergence.  -/
LSeries.abscissaOfAbsConv_congr' : ∀ {f g : ℕ → ℂ}, f =ᶠ[Filter.atTop] g → LSeries.abscissaOfAbsConv f = LSeries.abscissaOfAbsConv g
-- Mathlib.Analysis.Calculus.Deriv.MeanValue
/-- Cauchy's Mean Value Theorem, extended `deriv` version.  -/
exists_ratio_deriv_eq_ratio_slope' : ∀ (f : ℝ → ℝ) {a b : ℝ},
  a < b →
    ∀ (g : ℝ → ℝ) {lfa lga lfb lgb : ℝ},
      DifferentiableOn ℝ f (Set.Ioo a b) →
        DifferentiableOn ℝ g (Set.Ioo a b) →
          Filter.Tendsto f (nhdsWithin a (Set.Ioi a)) (nhds lfa) →
            Filter.Tendsto g (nhdsWithin a (Set.Ioi a)) (nhds lga) →
              Filter.Tendsto f (nhdsWithin b (Set.Iio b)) (nhds lfb) →
                Filter.Tendsto g (nhdsWithin b (Set.Iio b)) (nhds lgb) →
                  ∃ c ∈ Set.Ioo a b, (lgb - lga) * deriv f c = (lfb - lfa) * deriv g c
-- Mathlib.Topology.MetricSpace.HolderNorm
/-- If a function is `r`-Hölder over a bounded space, then it is also `s`-Hölder when `s ≤ r`.
See `MemHolder.of_le` for the version in a pseudometric space.  -/
MemHolder.of_le' : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] {r : NNReal} {f : X → Y}
  {s : NNReal}, MemHolder r f → s ≤ r → (∃ C, ∀ (x y : X), edist x y ≤ ↑C) → MemHolder s f
-- Mathlib.Order.Lattice
sup_congr_right : ∀ {α : Type u} [inst : SemilatticeSup α] {a b c : α}, a ≤ b ⊔ c → b ≤ a ⊔ c → a ⊔ c = b ⊔ c
-- Qq.Simp
/-- A copy of `Meta.Simp.Result.mk` with explicit types.  -/
Lean.Meta.Simp.ResultQ.mk : {u : Lean.Level} →
  {α : Q(Sort u)} →
    {e : Q(«$α»)} → (expr : Q(«$α»)) → Option Q(«$e» = «$expr») → optParam Bool true → Lean.Meta.Simp.ResultQ e
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
_private.Mathlib.Combinatorics.SimpleGraph.Walk.Operations.0.SimpleGraph.Walk.concatRecAux.match_1.eq_1 : ∀ {V : Type u_1} {G : SimpleGraph V} {u : V} (motive : (v : V) → G.Walk u v → Sort u_2)
  (h_1 : Unit → motive u SimpleGraph.Walk.nil)
  (h_2 : (v v_1 : V) → (h : G.Adj u v_1) → (p : G.Walk v_1 v) → motive v (SimpleGraph.Walk.cons h p)),
  (match u, SimpleGraph.Walk.nil with
    | .(u), SimpleGraph.Walk.nil => h_1 ()
    | v, SimpleGraph.Walk.cons h p => h_2 v v_1 h p) =
    h_1 ()
-- Mathlib.Probability.Kernel.Composition.ParallelComp
/-- Parallel product of two kernels.  -/
ProbabilityTheory.«term_∥ₖ_» : Lean.TrailingParserDescr
-- Init.Data.UInt.Bitwise
UInt8.left_le_or : ∀ {a b : UInt8}, a ≤ a ||| b
-- Init.Data.Int.Gcd
Int.eq_zero_of_lcm_eq_zero : ∀ {m n : ℤ}, m.lcm n = 0 → m = 0 ∨ n = 0
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.iIndepFun.indepFun_mul_left : ∀ {Ω : Type u_1} {ι : Type u_2} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {β : Type u_10}
  {m : MeasurableSpace β} [inst : Mul β] [MeasurableMul₂ β] {f : ι → Ω → β},
  ProbabilityTheory.iIndepFun f μ →
    (∀ (i : ι), Measurable (f i)) → ∀ (i j k : ι), i ≠ k → j ≠ k → ProbabilityTheory.IndepFun (f i * f j) (f k) μ
-- Mathlib.CategoryTheory.Category.Basic
/-- Notation for whiskering an equation by a morphism (on the left).
If `g h : Y ⟶ Z` and `w : g = h` and `f : X ⟶ Y`, then `f ≫= w : f ≫ g = f ≫ h`.
 -/
CategoryTheory.«term_≫=_» : Lean.TrailingParserDescr
-- Mathlib.Algebra.Group.Submonoid.Basic
AddSubmonoid.closure_empty : ∀ {M : Type u_1} [inst : AddZeroClass M], AddSubmonoid.closure ∅ = ⊥
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.Exact.op : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C}, S.Exact → S.op.Exact
-- Mathlib.RingTheory.Multiplicity
emultiplicity_ne_of_multiplicity_ne : ∀ {α : Type u_1} [inst : Monoid α] {a b : α} {n : ℕ}, multiplicity a b ≠ n → emultiplicity a b ≠ ↑n
-- Mathlib.Algebra.Order.Group.Multiset
Multiset.count_nsmul : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (n : ℕ) (s : Multiset α),
  Multiset.count a (n • s) = n * Multiset.count a s
-- Init.Data.String.Lemmas.FindPos
String.next_eq_posGT : ∀ {s : String} {p : s.Pos} {h : p ≠ s.endPos}, p.next h = s.posGT p.offset ⋯
-- Mathlib.Order.UpperLower.CompleteLattice
/-- An order isomorphism of Preorders induces an order isomorphism of their lower sets.  -/
LowerSet.map : {α : Type u_1} → {β : Type u_2} → [inst : Preorder α] → [inst_1 : Preorder β] → α ≃o β → LowerSet α ≃o LowerSet β
-- Mathlib.Data.List.AList
AList.empty_union : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {s : AList β}, ∅ ∪ s = s
-- Init.Data.List.Perm
List.Perm.swap' : ∀ {α : Type u_1} (x y : α) {l₁ l₂ : List α}, l₁.Perm l₂ → (y :: x :: l₁).Perm (x :: y :: l₂)
-- Mathlib.Topology.MetricSpace.Thickening
/-- The closure of a set equals the intersection of its closed thickenings of positive radii
accumulating at zero.  -/
Metric.closure_eq_iInter_cthickening' : ∀ {α : Type u} [inst : PseudoEMetricSpace α] (E : Set α) (s : Set ℝ),
  (∀ (ε : ℝ), 0 < ε → (s ∩ Set.Ioc 0 ε).Nonempty) → closure E = ⋂ δ ∈ s, Metric.cthickening δ E
-- Mathlib.LinearAlgebra.Dimension.Basic
Module.rank_def : ∀ (R : Type u_1) (M : Type u_2) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  Module.rank R M = ⨆ ι, Cardinal.mk ↑↑ι
-- Mathlib.Algebra.Homology.ShortComplex.Basic
/-- the third (right) object of a `ShortComplex`  -/
CategoryTheory.ShortComplex.X₃ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] → CategoryTheory.ShortComplex C → C
-- Mathlib.Algebra.ContinuedFractions.TerminatedStable
GenContFract.convs_stable_of_terminated : ∀ {K : Type u_1} {g : GenContFract K} {n m : ℕ} [inst : DivisionRing K],
  n ≤ m → g.TerminatedAt n → g.convs m = g.convs n
-- Mathlib.Data.Set.PowersetCard
Set.powersetCard.eq_empty_iff : ∀ {α : Type u_1} {n : ℕ} [Finite α], Set.powersetCard α n = ∅ ↔ Nat.card α < n
-- Mathlib.Topology.EMetricSpace.Defs
WeakPseudoEMetricSpace.ext_iff : ∀ {α : Type u_2} [inst : TopologicalSpace α] {m m' : WeakPseudoEMetricSpace α}, m = m' ↔ m.toEDist = m'.toEDist
-- Mathlib.Logic.Function.Basic
Function.LeftInverse.eq : ∀ {α : Sort u_1} {β : Sort u_2} {g : β → α} {f : α → β}, Function.LeftInverse g f → ∀ (x : α), g (f x) = x
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Unit.RcoSliceData.mk : {α : Type u} →
  [inst : Ord α] → (Std.DTreeMap.Internal.Impl α fun x => Unit) → Std.Rco α → Std.DTreeMap.Internal.Unit.RcoSliceData α
-- Aesop.RuleTac.Forward.Basic
Aesop.ForwardHypData.mk.inj : ∀ {depths depths_1 : Std.HashMap Lean.FVarId ℕ}, { depths := depths } = { depths := depths_1 } → depths = depths_1
-- Mathlib.Algebra.GradedMonoid
GradedMonoid.fst_pow : ∀ {ι : Type u_1} (A : ι → Type u_2) [inst : AddMonoid ι] [inst_1 : GradedMonoid.GMonoid A] (x : GradedMonoid A) (n : ℕ),
  (x ^ n).fst = n • x.fst
-- Mathlib.CategoryTheory.Join.Sum
CategoryTheory.Join.inlCompFromSum_inv_app : ∀ (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] (X : C),
  (CategoryTheory.Join.inlCompFromSum C D).inv.app X = CategoryTheory.CategoryStruct.id (CategoryTheory.Join.left X)
-- Mathlib.RingTheory.GradedAlgebra.Basic
DirectSum.coe_decompose_mul_of_right_mem_of_le : ∀ {ι : Type u_1} {A : Type u_3} {σ : Type u_4} [inst : Semiring A] [inst_1 : DecidableEq ι] [inst_2 : AddCommMonoid ι]
  [inst_3 : PartialOrder ι] [CanonicallyOrderedAdd ι] [inst_5 : SetLike σ A] [inst_6 : AddSubmonoidClass σ A]
  (𝒜 : ι → σ) [inst_7 : GradedRing 𝒜] {a b : A} {n i : ι} [inst_8 : Sub ι] [OrderedSub ι] [AddLeftReflectLE ι],
  b ∈ 𝒜 i → i ≤ n → ↑(((DirectSum.decompose 𝒜) (a * b)) n) = ↑(((DirectSum.decompose 𝒜) a) (n - i)) * b
-- Mathlib.Algebra.Order.Interval.Basic
Interval.addCommMonoid.eq_1 : ∀ {α : Type u_2} [inst : AddCommMonoid α] [inst_1 : Preorder α] [inst_2 : IsOrderedAddMonoid α],
  Interval.addCommMonoid =
    { toAdd := Interval.addZeroClass.toAdd, add_assoc := ⋯, toZero := Interval.addZeroClass.toZero, zero_add := ⋯,
      add_zero := ⋯, nsmul := nsmulRecAuto, nsmul_zero := ⋯, nsmul_succ := ⋯, add_comm := ⋯ }
-- Mathlib.Data.Ordmap.Ordset
_private.Mathlib.Data.Ordmap.Ordset.0.Ordnode.adjustWith.match_1.splitter : {α : Type u_1} →
  (motive : Ordnode α → Sort u_2) →
    (x : Ordnode α) →
      (Unit → motive Ordnode.nil) →
        ((sz : ℕ) → (l : Ordnode α) → (y : α) → (r : Ordnode α) → motive (Ordnode.node sz l y r)) → motive x
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
CategoryTheory.Limits.FormalCoproduct.fromIncl_comp_coproductIsoSelf_inv_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Limits.FormalCoproduct C) (i : X.I)
  {Z : CategoryTheory.Limits.FormalCoproduct C} (h : ∐ X.toFun ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.FormalCoproduct.Hom.fromIncl i (CategoryTheory.CategoryStruct.id (X.obj i)))
      (CategoryTheory.CategoryStruct.comp X.coproductIsoSelf.inv h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι X.toFun i) h
-- Mathlib.CategoryTheory.Limits.Shapes.Preorder.HasIterationOfShape
CategoryTheory.Limits.hasColimitsOfShape_of_initialSeg : ∀ {J : Type w} [inst : LinearOrder J] (C : Type u) [inst_1 : CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasIterationOfShape J C] [SuccOrder J] [WellFoundedLT J] {α : Type u_1}
  [inst_5 : PartialOrder α] (f : α ≤i J) [Nonempty α], CategoryTheory.Limits.HasColimitsOfShape α C
-- Mathlib.LinearAlgebra.TensorProduct.Tower
/-- This version enables better pattern matching via the tactic `obtain`.  -/
Submodule.toBaseChange_surjective' : ∀ {R : Type u_1} {M : Type u_2} (A : Type u_3) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] (p : Submodule R M) {y : TensorProduct R A M},
  y ∈ Submodule.baseChange A p → ∃ x, ↑((Submodule.toBaseChange A p) x) = y
-- Mathlib.Topology.Algebra.Algebra
/-- This is really a statement about topological algebra isomorphisms,
but we don't have those, so we use the clunky approach of talking about
an algebra homomorphism, and a separate homeomorphism,
along with a witness that as functions they are the same.
 -/
Subalgebra.topologicalClosure_comap_homeomorph : ∀ {R : Type u_1} [inst : CommSemiring R] {A : Type u} [inst_1 : TopologicalSpace A] [inst_2 : Semiring A]
  [inst_3 : Algebra R A] [inst_4 : IsSemitopologicalSemiring A] (s : Subalgebra R A) {B : Type u_2}
  [inst_5 : TopologicalSpace B] [inst_6 : Ring B] [inst_7 : IsSemitopologicalRing B] [inst_8 : Algebra R B]
  (f : B →ₐ[R] A) (f' : B ≃ₜ A),
  ⇑f = ⇑f' → Subalgebra.comap f s.topologicalClosure = (Subalgebra.comap f s).topologicalClosure
-- Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
CategoryTheory.Triangulated.TStructure.eTruncLTLTIsoLT_inv_hom_id_app_eTruncLT_obj : ∀ {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.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) [inst_6 : CategoryTheory.IsTriangulated C] (a b : EInt) (hab : b ≤ a)
  (X : C),
  CategoryTheory.CategoryStruct.comp ((t.eTruncLTLTIsoLT a b hab).inv.app ((t.eTruncLT.obj a).obj X))
      ((t.eTruncLT.obj b).map ((t.eTruncLT.obj a).map ((t.eTruncLTι a).app X))) =
    CategoryTheory.CategoryStruct.id ((t.eTruncLT.obj b).obj ((t.eTruncLT.obj a).obj X))
-- Mathlib.Data.Set.Function
Set.MapsTo.mem_iff : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β},
  Set.MapsTo f s t → Set.MapsTo f sᶜ tᶜ → ∀ {x : α}, f x ∈ t ↔ x ∈ s
-- Mathlib.Algebra.Category.Semigrp.Basic
Semigrp.hom_inv_apply : ∀ {X Y : Semigrp} (e : X ≅ Y) (s : ↑Y),
  (CategoryTheory.ConcreteCategory.hom e.hom) ((CategoryTheory.ConcreteCategory.hom e.inv) s) = s
-- Mathlib.RingTheory.Ideal.Over
Ideal.Quotient.tower_quotient_map_quotient : ∀ {R : Type u_1} [inst : CommRing R] {S : Type u_2} [inst_1 : CommRing S] {p : Ideal R} [inst_2 : Algebra R S],
  IsScalarTower R (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)
-- Lean.Data.Lsp.Extra
Lean.Lsp.RpcConnected.mk.inj : ∀ {sessionId sessionId_1 : UInt64}, { sessionId := sessionId } = { sessionId := sessionId_1 } → sessionId = sessionId_1
-- Lean.LocalContext
/-- A local variable without any value.
`Lean.LocalContext.mkBinding` creates lambdas or foralls from `cdecl`s.  -/
Lean.LocalDecl.cdecl : ℕ → Lean.FVarId → Lean.Name → Lean.Expr → Lean.BinderInfo → Lean.LocalDeclKind → Lean.LocalDecl
-- Lean.Elab.InfoTree.Types
Lean.Elab.PartialTermInfo.toElabInfo : Lean.Elab.PartialTermInfo → Lean.Elab.ElabInfo
-- Mathlib.Algebra.Group.Commute.Defs
AddCommute.zero_left : ∀ {M : Type u_2} [inst : AddZeroClass M] (a : M), AddCommute 0 a
-- Mathlib.Algebra.Category.Ring.Basic
/-- The category of commutative rings.  -/
CommRingCat : Type (u + 1)
-- Std.Http.Internal.IndexMultiMap
Std.Internal.instInhabitedIndexMultiMap : {α : Type u_1} →
  {β : Type u_2} →
    [inst : BEq α] → [inst_1 : Hashable α] → [Inhabited α] → [Inhabited β] → Inhabited (Std.Internal.IndexMultiMap α β)
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.toAffineMap_injective : ∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : AddCommGroup V₂] [inst_3 : Module k V₁] [inst_4 : Module k V₂]
  [inst_5 : AddTorsor V₁ P₁] [inst_6 : AddTorsor V₂ P₂], Function.Injective AffineEquiv.toAffineMap
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.minD_empty : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {fallback : α}, ∅.minD fallback = fallback
-- Mathlib.RingTheory.HahnSeries.Addition
HahnSeries.instSMulZeroClass : {Γ : Type u_1} →
  {R : Type u_3} →
    [inst : PartialOrder Γ] →
      {V : Type u_8} → [inst_1 : Zero V] → [SMulZeroClass R V] → SMulZeroClass R (HahnSeries Γ V)
-- Init.Data.String.Extra
/-- Checks whether an array of bytes is a valid UTF-8 encoding of a string.
 -/
String.validateUTF8 : ByteArray → Bool
-- Mathlib.Dynamics.BirkhoffSum.Average
/-- Birkhoff average is "almost invariant" under `f`:
the difference between `birkhoffAverage R f g n (f x)` and `birkhoffAverage R f g n x`
is equal to `(n : R)⁻¹ • (g (f^[n] x) - g x)`.  -/
birkhoffAverage_apply_sub_birkhoffAverage : ∀ {R : Type u_1} {α : Type u_2} {M : Type u_3} [inst : DivisionSemiring R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] (f : α → α) (g : α → M) (n : ℕ) (x : α),
  birkhoffAverage R f g n (f x) - birkhoffAverage R f g n x = (↑n)⁻¹ • (g (f^[n] x) - g x)
-- Init.Data.String.Lemmas.Pattern.TakeDrop.String
String.Slice.skipPrefix?_string_eq_some_iff : ∀ {pat : String} {s : String.Slice} {pos : s.Pos}, s.skipPrefix? pat = some pos ↔ ∃ t, pos.Splits pat t
-- Mathlib.Computability.Partrec
Partrec.optionCasesOn_right : ∀ {α : Type u_1} {β : Type u_2} {σ : Type u_4} [inst : Primcodable α] [inst_1 : Primcodable β] [inst_2 : Primcodable σ]
  {o : α → Option β} {f : α → σ} {g : α → β →. σ},
  Computable o → Computable f → Partrec₂ g → Partrec fun a => Option.casesOn (o a) (Part.some (f a)) (g a)
-- Mathlib.Analysis.Complex.Trigonometric
Complex.ofReal_cot : ∀ (x : ℝ), ↑x.cot = (↑x).cot
-- Lean.Declaration
/-- List of the names of the constructors for this inductive datatype.  -/
Lean.InductiveVal.ctors : Lean.InductiveVal → List Lean.Name
-- Mathlib.CategoryTheory.Sites.Descent.DescentData
CategoryTheory.Pseudofunctor.DescentData.Hom.ext_iff : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C}
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} {ι : Type t} {S : C}
  {X : ι → C} {f : (i : ι) → X i ⟶ S} {D₁ D₂ : F.DescentData f} {x y : D₁.Hom D₂}, x = y ↔ x.hom = y.hom
-- Mathlib.Topology.EMetricSpace.Defs
/-- **Alias** of `Metric.exists_eball_subset_eball`. -/
EMetric.exists_ball_subset_ball : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {x y : α} {ε : ENNReal},
  y ∈ Metric.eball x ε → ∃ ε' > 0, Metric.eball y ε' ⊆ Metric.eball x ε
-- Mathlib.Order.ModularLattice
DistribLattice.instIsModularLattice : ∀ {α : Type u_1} [inst : DistribLattice α], IsModularLattice α
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.UseImplicitLambdaResult.yes.inj : ∀ {expectedType expectedType_1 : Lean.Expr},
  Lean.Elab.Term.UseImplicitLambdaResult.yes expectedType = Lean.Elab.Term.UseImplicitLambdaResult.yes expectedType_1 →
    expectedType = expectedType_1
-- Mathlib.Analysis.Calculus.FDeriv.Measurable
/-- The set `B f K r s ε` is the set of points `x` around which there exists a vector
`L` belonging to `K` (a given set of vectors) such that `h • L` approximates well `f (x + h)`
(up to an error `ε`), simultaneously at scales `r` and `s`.  -/
RightDerivMeasurableAux.B : {F : Type u_1} → [inst : NormedAddCommGroup F] → [NormedSpace ℝ F] → (ℝ → F) → Set F → ℝ → ℝ → ℝ → Set ℝ
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.mem_mul : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Mul α] {s t : Finset α} {x : α},
  x ∈ s * t ↔ ∃ y ∈ s, ∃ z ∈ t, y * z = x
-- Mathlib.ModelTheory.Encoding
_private.Mathlib.ModelTheory.Encoding.0.FirstOrder.Language.BoundedFormula.listEncode.match_1.splitter : {L : FirstOrder.Language} →
  {α : Type u_3} →
    (motive : (x : ℕ) → L.BoundedFormula α x → Sort u_4) →
      (x : ℕ) →
        (x_1 : L.BoundedFormula α x) →
          ((n : ℕ) → motive n FirstOrder.Language.BoundedFormula.falsum) →
            ((x : ℕ) → (t₁ t₂ : L.Term (α ⊕ Fin x)) → motive x (FirstOrder.Language.BoundedFormula.equal t₁ t₂)) →
              ((n l : ℕ) →
                  (R : L.Relations l) →
                    (ts : Fin l → L.Term (α ⊕ Fin n)) → motive n (FirstOrder.Language.BoundedFormula.rel R ts)) →
                ((x : ℕ) → (φ₁ φ₂ : L.BoundedFormula α x) → motive x (φ₁.imp φ₂)) →
                  ((x : ℕ) → (φ : L.BoundedFormula α (x + 1)) → motive x φ.all) → motive x x_1
-- Mathlib.Order.LiminfLimsup
Filter.limsSup_top : ∀ {α : Type u_1} [inst : CompleteLattice α], ⊤.limsSup = ⊤
-- Mathlib.CategoryTheory.GradedObject.Monoidal
CategoryTheory.GradedObject.instFiniteElemProdNatOfPredEqHAddFstSnd : ∀ (n : ℕ), Finite ↑{i | i.1 + i.2.1 + i.2.2 = n}
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.IdealSheafData.radical_sup : ∀ {X : AlgebraicGeometry.Scheme} {I J : X.IdealSheafData}, (I ⊔ J).radical = (I.radical ⊔ J.radical).radical
-- Mathlib.Analysis.Convex.Side
AffineSubspace.sOppSide_pointReflection : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Field R] [inst_1 : LinearOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P]
  {s : AffineSubspace R P} {x y : P}, x ∈ s → y ∉ s → s.SOppSide y ((AffineEquiv.pointReflection R x) y)
-- Init.Data.UInt.Lemmas
UInt8.mul_def : ∀ (a b : UInt8), a * b = { toBitVec := a.toBitVec * b.toBitVec }