mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.DiscrTree.Util
/-- Get the number of values stored in a `DiscrTree`. O(n) in the size of the tree.
 -/
Lean.Meta.DiscrTree.size : {α : Type} → Lean.Meta.DiscrTree α → ℕ
-- Mathlib.NumberTheory.Padics.RingHoms
PadicInt.limNthHom_mul : ∀ {R : Type u_1} [inst : NonAssocSemiring R] {p : ℕ} {f : (k : ℕ) → R →+* ZMod (p ^ k)} [hp_prime : Fact (Nat.Prime p)]
  (f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1) (r s : R),
  PadicInt.limNthHom f_compat (r * s) = PadicInt.limNthHom f_compat r * PadicInt.limNthHom f_compat s
-- Mathlib.Analysis.Convex.Side
/-- **Alias** of the forward direction of `AffineSubspace.sSameSide_comm`. -/
AffineSubspace.SSameSide.symm : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : CommRing R] [inst_1 : PartialOrder 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}, s.SSameSide x y → s.SSameSide y x
-- Lean.Meta.AppBuilder
/-- Returns a proof for `p : Prop` using `decide p`  -/
Lean.Meta.mkDecideProof : Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
/-- A right fraction from `X : C` to `Y : C` for `W : MorphismProperty C` consists of the
datum of an object `X' : C` and maps `s : X' ⟶ X` and `f : X' ⟶ Y` such that `W s`.  -/
CategoryTheory.MorphismProperty.RightFraction : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] → CategoryTheory.MorphismProperty C → C → C → Type (max u_1 v_1)
-- Init.Prelude
/-- An exception in the `MacroM` monad.  -/
Lean.Macro.Exception : Type
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
/-- `QuadraticMap R M N` inherits the scalar action from any algebra over `R`.

This provides an `R`-action via `Algebra.id`.  -/
QuadraticMap.instSMul : {S : Type u_1} →
  {R : Type u_3} →
    {M : Type u_4} →
      {N : Type u_5} →
        [inst : CommSemiring R] →
          [inst_1 : AddCommMonoid M] →
            [inst_2 : Module R M] →
              [inst_3 : AddCommMonoid N] →
                [inst_4 : Module R N] →
                  [inst_5 : Monoid S] →
                    [inst_6 : DistribMulAction S N] → [SMulCommClass S R N] → SMul S (QuadraticMap R M N)
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.uniqueHomFromTrivial : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      (A : CategoryTheory.AddMon C) → Unique (CategoryTheory.AddMon.trivial C ⟶ A)
-- Mathlib.Analysis.InnerProductSpace.EuclideanDist
Euclidean.exists_pos_lt_subset_ball : ∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : TopologicalSpace E] [inst_2 : IsTopologicalAddGroup E]
  [inst_3 : T2Space E] [inst_4 : Module ℝ E] [inst_5 : ContinuousSMul ℝ E] [inst_6 : FiniteDimensional ℝ E] {R : ℝ}
  {s : Set E} {x : E}, 0 < R → IsClosed s → s ⊆ Euclidean.ball x R → ∃ r ∈ Set.Ioo 0 R, s ⊆ Euclidean.ball x r
-- Mathlib.Algebra.Category.Grp.Basic
/-- Build an `AddEquiv` from an isomorphism in the category `AddCommGrpCat`.  -/
CategoryTheory.Iso.addCommGroupIsoToAddEquiv : {X Y : AddCommGrpCat} → (X ≅ Y) → ↑X ≃+ ↑Y
-- Std.Time.Date.Unit.Weekday
Std.Time.Weekday.instLTOrdinal : LT Std.Time.Weekday.Ordinal
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
/-- If `F` admits a pointwise right Kan extension along `L`, then any right Kan extension of `F`
along `L` is a pointwise right Kan extension.  -/
CategoryTheory.Functor.isPointwiseRightKanExtensionOfIsRightKanExtension : {C : Type u_1} →
  {D : Type u_2} →
    {H : Type u_4} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
          [inst_2 : CategoryTheory.Category.{v_4, u_4} H] →
            {L : CategoryTheory.Functor C D} →
              {F : CategoryTheory.Functor C H} →
                [L.HasPointwiseRightKanExtension F] →
                  (F' : CategoryTheory.Functor D H) →
                    (α : L.comp F' ⟶ F) →
                      [F'.IsRightKanExtension α] →
                        (CategoryTheory.Functor.RightExtension.mk F' α).IsPointwiseRightKanExtension
-- Mathlib.Algebra.Homology.HomologySequence
HomologicalComplex.HomologySequence.instMonoMap'ComposableArrows₃OfNatNat : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {c : ComplexShape ι} (K : HomologicalComplex C c) (i j : ι) [inst_2 : K.HasHomology i] [inst_3 : K.HasHomology j],
  CategoryTheory.Mono
    ((HomologicalComplex.HomologySequence.composableArrows₃ K i j).map' 0 1
      HomologicalComplex.HomologySequence.instMonoMap'ComposableArrows₃OfNatNat._proof_1
      HomologicalComplex.HomologySequence.instMonoMap'ComposableArrows₃OfNatNat._proof_3)
-- Mathlib.Topology.Sets.VietorisTopology
TopologicalSpace.vietoris.continuous_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → Set β},
  Continuous f ↔ (∀ (U : Set β), IsOpen U → IsOpen (f ⁻¹' 𝒫 U)) ∧ ∀ (F : Set β), IsClosed F → IsClosed (f ⁻¹' 𝒫 F)
-- Mathlib.CategoryTheory.Abelian.Transfer
CategoryTheory.AsSmall.instAdditiveUp : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C],
  CategoryTheory.AsSmall.up.Additive
-- Mathlib.Algebra.Module.LocalizedModule.Submodule
Submodule.localized'.congr_simp : ∀ {R : Type u_1} (S : Type u_2) {M : Type u_3} {N : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid N] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : Algebra R S] [inst_7 : Module S N] [inst_8 : IsScalarTower R S N] (p p_1 : Submonoid R) (e_p : p = p_1)
  [inst_9 : IsLocalization p S] (f f_1 : M →ₗ[R] N) (e_f : f = f_1) [inst_10 : IsLocalizedModule p f]
  (M' M'_1 : Submodule R M), M' = M'_1 → Submodule.localized' S p f M' = Submodule.localized' S p_1 f_1 M'_1
-- Mathlib.AlgebraicGeometry.ResidueField
AlgebraicGeometry.Scheme.residue_residueFieldCongr_assoc : ∀ (X : AlgebraicGeometry.Scheme) {x y : ↥X} (h : x = y) {Z : CommRingCat} (h_1 : X.residueField y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.residue x)
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.residueFieldCongr h).hom h_1) =
    CategoryTheory.CategoryStruct.comp (X.presheaf.stalkCongr ⋯).hom
      (CategoryTheory.CategoryStruct.comp (X.residue y) h_1)
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
CategoryTheory.Oplax.LaxTrans.Modification.mk.inj : ∀ {B : Type u₁} {inst : CategoryTheory.Bicategory B} {C : Type u₂} {inst_1 : CategoryTheory.Bicategory C}
  {F G : CategoryTheory.OplaxFunctor B C} {η θ : F ⟶ G} {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.Oplax.LaxTrans.Modification.naturality._autoParam}
  {app_1 : (a : B) → η.app a ⟶ θ.app a}
  {naturality_1 :
    autoParam
      (∀ {a b : B} (f : a ⟶ b),
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (app_1 a) (G.map f))
            (θ.naturality f) =
          CategoryTheory.CategoryStruct.comp (η.naturality f)
            (CategoryTheory.Bicategory.whiskerLeft (F.map f) (app_1 b)))
      CategoryTheory.Oplax.LaxTrans.Modification.naturality._autoParam},
  { app := app, naturality := naturality } = { app := app_1, naturality := naturality_1 } → app = app_1
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CompletionItem.tags? : Lean.Lsp.CompletionItem → Option (Array Lean.Lsp.CompletionItemTag)
-- Mathlib.Order.Monotone.Basic
/-- **Alias** of the reverse direction of `antitone_comp_ofDual_iff`. -/
Monotone.dual_left : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
  Monotone f → Antitone (f ∘ ⇑OrderDual.ofDual)
-- Mathlib.RingTheory.FreeCommRing
FreeCommRing.isSupported_add : ∀ {α : Type u} {x y : FreeCommRing α} {s : Set α}, x.IsSupported s → y.IsSupported s → (x + y).IsSupported s
-- Mathlib.Algebra.Order.Group.Synonym
OrderDual.instAddCommGroup.eq_1 : ∀ {α : Type u_1} [inst : AddCommGroup α],
  OrderDual.instAddCommGroup = { toAddGroup := OrderDual.instAddGroup, add_comm := ⋯ }
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.compare_maxKey_modify_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {k : α} {f : β → β} {he : Std.ExtDTreeMap.Const.modify t k f ≠ ∅},
  cmp ((Std.ExtDTreeMap.Const.modify t k f).maxKey he) (t.maxKey ⋯) = Ordering.eq
-- Init.Omega.Constraint
Lean.Omega.Constraint.neg.eq_1 : ∀ (c : Lean.Omega.Constraint), c.neg = c.flip.map fun x => -x
-- Mathlib.Analysis.SpecialFunctions.Integrals.Basic
integral_inv : ∀ {a b : ℝ}, 0 ∉ Set.uIcc a b → ∫ (x : ℝ) in a..b, x⁻¹ = Real.log (b / a)
-- Mathlib.RingTheory.Valuation.ValuationRing
ValuationRing.linearOrderedCommGroupWithZero : (A : Type u) →
  [inst : CommRing A] →
    (K : Type v) →
      [inst_1 : Field K] →
        [inst_2 : Algebra A K] →
          [inst_3 : IsDomain A] →
            [ValuationRing A] → [IsFractionRing A K] → LinearOrderedCommGroupWithZero (ValuationRing.ValueGroup A K)
-- Mathlib.CategoryTheory.Functor.OfSequence
CategoryTheory.Functor.OfSequence.map.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (x : ℕ → C) (x_1 : (n : ℕ) → x n ⟶ x (n + 1)),
  CategoryTheory.Functor.OfSequence.map x_1 0 0 = fun x_2 => CategoryTheory.CategoryStruct.id (x 0)
-- LeanSearchClient.Syntax
LeanSearchClient.SearchResult.mk.sizeOf_spec : ∀ (name : String) (type? docString? doc_url? kind? : Option String),
  sizeOf { name := name, type? := type?, docString? := docString?, doc_url? := doc_url?, kind? := kind? } =
    1 + sizeOf name + sizeOf type? + sizeOf docString? + sizeOf doc_url? + sizeOf kind?
-- Mathlib.Algebra.Star.Subsemiring
StarSubsemiring.copy_eq : ∀ {R : Type v} [inst : NonAssocSemiring R] [inst_1 : StarRing R] (S : StarSubsemiring R) (s : Set R) (hs : s = ↑S),
  S.copy s hs = S
-- Mathlib.Order.Filter.Germ.Basic
/-- Given two germs `f : Germ l β`, and `g : Germ lc α`, where `l : Filter α`, if `g` tends to `l`,
then the composition `f ∘ g` is well-defined as a germ at `lc`.  -/
Filter.Germ.compTendsto' : {α : Type u_1} →
  {β : Type u_2} →
    {γ : Type u_3} → {l : Filter α} → l.Germ β → {lc : Filter γ} → (g : lc.Germ α) → g.Tendsto l → lc.Germ β
-- Mathlib.Algebra.Module.LocalizedModule.Basic
LocalizedModule.algebra' : {R : Type u} →
  [inst : CommSemiring R] →
    {S : Submonoid R} →
      {A : Type u_3} → [inst_1 : Semiring A] → [inst_2 : Algebra R A] → Algebra R (LocalizedModule S A)
-- Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup
/-- This is another version of `conjAct_smul_ι_mem_range_ι` which uses `involute`.  -/
pinGroup.involute_act_ι_mem_range_ι : ∀ {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 : (CliffordAlgebra Q)ˣ},
  ↑x ∈ pinGroup Q →
    ∀ [Invertible 2] (y : M), CliffordAlgebra.involute ↑x * (CliffordAlgebra.ι Q) y * ↑x⁻¹ ∈ (CliffordAlgebra.ι Q).range
-- Mathlib.Data.Finset.Grade
Finset.val_wcovBy_val : ∀ {α : Type u_1} {s t : Finset α}, s.val ⩿ t.val ↔ s ⩿ t
-- Mathlib.Data.Tree.Basic
/-- The number of leaves of a binary tree  -/
BinaryTree.numLeaves : {α : Type u} → BinaryTree α → ℕ
-- Init.Data.BitVec.Bitblast
/-- The value of shifting right by `wn - 1` equals shifting by `wn` and grabbing the lsb at `(wn - 1)`.  -/
BitVec.DivModState.toNat_shiftRight_sub_one_eq : ∀ {w : ℕ} {args : BitVec.DivModArgs w} {qr : BitVec.DivModState w},
  BitVec.DivModState.Poised args qr →
    args.n.toNat >>> (qr.wn - 1) = args.n.toNat >>> qr.wn * 2 + (args.n.getLsbD (qr.wn - 1)).toNat
-- ProofWidgets.Presentation.Expr
ProofWidgets.ExprPresentations.presentations : ProofWidgets.ExprPresentations → Array ProofWidgets.ExprPresentationData
-- Mathlib.Algebra.Group.Even
even_iff_exists_add_self : ∀ {α : Type u_2} [inst : Add α] (a : α), Even a ↔ ∃ r, a = r + r
-- Mathlib.Algebra.Lie.Subalgebra
/-- The range of a morphism of Lie algebras is a Lie subalgebra.  -/
LieHom.range : {R : Type u} →
  {L : Type v} →
    [inst : CommRing R] →
      [inst_1 : LieRing L] →
        [inst_2 : LieAlgebra R L] →
          {L₂ : Type w} → [inst_3 : LieRing L₂] → [inst_4 : LieAlgebra R L₂] → (L →ₗ⁅R⁆ L₂) → LieSubalgebra R L₂
-- Lean.Meta.Tactic.Grind.Types
/-- Used to generate trace messages of the for `[grind] working on <tag>`,
and implement the macro `trace_goal`.
 -/
Lean.Meta.Grind.State.lastTag : Lean.Meta.Grind.State → Lean.Name
-- Lean.Meta.Sym.Apply
Lean.Meta.Sym.BackwardRule.mk.inj : ∀ {expr : Lean.Expr} {pattern : Lean.Meta.Sym.Pattern} {resultPos : List ℕ} {expr_1 : Lean.Expr}
  {pattern_1 : Lean.Meta.Sym.Pattern} {resultPos_1 : List ℕ},
  { expr := expr, pattern := pattern, resultPos := resultPos } =
      { expr := expr_1, pattern := pattern_1, resultPos := resultPos_1 } →
    expr = expr_1 ∧ pattern = pattern_1 ∧ resultPos = resultPos_1
-- Mathlib.Analysis.Normed.Group.Basic
dist_one : ∀ {E : Type u_5} [inst : SeminormedGroup E], dist 1 = norm
-- Mathlib.Algebra.Category.MonCat.Colimits
MonCat.Colimits.Relation.below.trans : ∀ {J : Type v} [inst : CategoryTheory.Category.{u, v} J] {F : CategoryTheory.Functor J MonCat}
  {motive : (a a_1 : MonCat.Colimits.Prequotient F) → MonCat.Colimits.Relation F a a_1 → Prop}
  (x y z : MonCat.Colimits.Prequotient F) (x_1 : MonCat.Colimits.Relation F x y) (x_2 : MonCat.Colimits.Relation F y z),
  MonCat.Colimits.Relation.below x_1 →
    motive x y x_1 → MonCat.Colimits.Relation.below x_2 → motive y z x_2 → MonCat.Colimits.Relation.below ⋯
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getD_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  [inst : BEq α] [Std.LawfulBEqOrd α] (h : t.WF) {l : List (α × β)} {k : α} {fallback : β},
  (List.map Prod.fst l).contains k = false →
    Std.DTreeMap.Internal.Impl.Const.getD (↑(Std.DTreeMap.Internal.Impl.Const.insertMany t l ⋯)) k fallback =
      Std.DTreeMap.Internal.Impl.Const.getD t k fallback
-- Mathlib.Analysis.Calculus.FDeriv.ContinuousAlternatingMap
ContinuousAlternatingMap.hasStrictFDerivAt : ∀ {𝕜 : Type u_1} {ι : Type u_2} {E : Type u_3} {F : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : Fintype ι] [inst_6 : DecidableEq ι] (f : E [⋀^ι]→L[𝕜] F) (x : ι → E),
  HasStrictFDerivAt (⇑f) (f.linearDeriv x) x
-- Mathlib.NumberTheory.SelbergSieve
/-- We set up a sieve problem as follows. Take a finite set of natural numbers `A`, whose elements
are weighted by a sequence `a n`. Also take a finite set of primes `P`, represented by a squarefree
natural number. These are the primes that we will sift from our set `A`. Suppose we can approximate
`∑ n ∈ A with d ∣ n, a n = ν d * X + R d`, where `X` is an approximation to the total size of `A`
and `ν` is a multiplicative arithmetic function such that `0 < ν p < 1` for all primes `p ∣ P`.

Then a sieve-type theorem will give us an upper (or lower) bound on the size of the sifted sum
`∑ n ∈ support with n.Coprime P, a n`, obtained by removing any elements of `A` that are a
multiple of a prime in `P`.  -/
BoundingSieve : Type
-- Mathlib.GroupTheory.MonoidLocalization.Basic
Submonoid.LocalizationMap.instIsCancelMulLocalization : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} [IsCancelMul M], IsCancelMul (Localization S)
-- Mathlib.AlgebraicGeometry.Birational.RationalMap
AlgebraicGeometry.Scheme.PartialMap.instIsOverToPartialMapOfIsOver : ∀ {X Y S : AlgebraicGeometry.Scheme} [inst : X.Over S] [inst_1 : Y.Over S] (f : X ⟶ Y)
  [AlgebraicGeometry.Scheme.Hom.IsOver f S],
  AlgebraicGeometry.Scheme.PartialMap.IsOver S (AlgebraicGeometry.Scheme.Hom.toPartialMap f)
-- Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Module.FaithfullyFlat.subsingleton_tensorProduct_iff_left : ∀ (R : Type u) (M : Type v) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {N : Type u_1}
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] [Module.FaithfullyFlat R N],
  Subsingleton (TensorProduct R M N) ↔ Subsingleton M
-- Mathlib.Algebra.BigOperators.Group.Multiset.Defs
Multiset.sum_replicate : ∀ {M : Type u_3} [inst : AddCommMonoid M] (n : ℕ) (a : M), (Multiset.replicate n a).sum = n • a
-- Mathlib.Tactic.Abel
/-- A type synonym used by `abel` to represent `n • x + a` in an additive commutative group.  -/
Mathlib.Tactic.Abel.termg : {α : Type u_1} → [AddCommGroup α] → ℤ → α → α → α
-- Lean.Parser.Basic
Lean.Parser.finishCommentBlock : Bool → ℕ → Lean.Parser.ParserFn
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
/-- If all elements of `s : Set A` commute pairwise, then `adjoin R s` is commutative.  -/
Algebra.isMulCommutative_adjoin : ∀ (R : Type uR) {A : Type uA} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] {s : Set A},
  (∀ x ∈ s, ∀ y ∈ s, x * y = y * x) → IsMulCommutative ↥(Algebra.adjoin R s)
-- Mathlib.Analysis.Seminorm
/-- A seminorm is continuous if `p.closedBall 0 r ∈ 𝓝 0` for *all* `r > 0`.
Over a `NontriviallyNormedField` it is actually enough to check that this is true
for *some* `r`, see `Seminorm.continuous'`.  -/
Seminorm.continuous_of_forall' : ∀ {𝕝 : Type u_6} {E : Type u_7} [inst : SeminormedRing 𝕝] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕝 E]
  [inst_3 : TopologicalSpace E] [IsTopologicalAddGroup E] {p : Seminorm 𝕝 E},
  (∀ r > 0, p.closedBall 0 r ∈ nhds 0) → Continuous ⇑p
-- Mathlib.Order.Hom.Lattice
LatticeHom.coe_toInfHom : ∀ {α : Type u_2} {β : Type u_3} [inst : Lattice α] [inst_1 : Lattice β] (f : LatticeHom α β), ⇑f.toInfHom = ⇑f
-- Mathlib.Algebra.Star.StarRingHom
NonUnitalStarRingHom.comp_id : ∀ {A : Type u_1} {B : Type u_2} [inst : NonUnitalNonAssocSemiring A] [inst_1 : Star A]
  [inst_2 : NonUnitalNonAssocSemiring B] [inst_3 : Star B] (f : A →⋆ₙ+* B), f.comp (NonUnitalStarRingHom.id A) = f
-- Mathlib.Analysis.Fourier.Notation
FourierModule.fourier_add : ∀ {R : Type u_5} {E : Type u_6} {F : outParam (Type u_7)} [inst : Add E] [inst_1 : Add F] [inst_2 : SMul R E]
  [inst_3 : SMul R F] (self : FourierModule R E F) (f g : E),
  FourierTransform.fourier (f + g) = FourierTransform.fourier f + FourierTransform.fourier g
-- Mathlib.RingTheory.Ideal.Quotient.Operations
Ideal.quotientEquiv_apply : ∀ {R : Type u} [inst : Ring R] {S : Type v} [inst_1 : Ring S] (I : Ideal R) (J : Ideal S) [inst_2 : I.IsTwoSided]
  [inst_3 : J.IsTwoSided] (f : R ≃+* S) (hIJ : J = Ideal.map (↑f) I) (a : R ⧸ I),
  (I.quotientEquiv J f hIJ) a = (↑↑(Ideal.quotientMap J ↑f ⋯)).toFun a
-- Init.Data.String.Basic
/-- Given a string `s`, turns a valid position on the slice `s.toSlice` into a valid position on the
string `s`.  -/
String.Pos.ofToSlice : {s : String} → s.toSlice.Pos → s.Pos
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.get?_erase : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k a : α},
  Std.ExtDHashMap.Const.get? (m.erase k) a = if (k == a) = true then none else Std.ExtDHashMap.Const.get? m a
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.typein_ordinal : ∀ (o : Ordinal.{u}), (Ordinal.typein LT.lt).toRelEmbedding o = Ordinal.lift.{u + 1, u} o
-- Mathlib.Logic.Equiv.Multiset
Denumerable.lower_raise : ∀ (l : List ℕ) (n : ℕ), Denumerable.lower (Denumerable.raise l n) n = l
-- Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Complex.betaIntegral_scaled : ∀ (s t : ℂ) {a : ℝ}, 0 < a → ∫ (x : ℝ) in 0..a, ↑x ^ (s - 1) * (↑a - ↑x) ^ (t - 1) = ↑a ^ (s + t - 1) * s.betaIntegral t
-- Mathlib.Algebra.Order.ToIntervalMod
toIcoMod_add_ofNat_mul : ∀ {R : Type u_1} [inst : NonAssocRing R] [inst_1 : LinearOrder R] [inst_2 : IsOrderedAddMonoid R]
  [inst_3 : Archimedean R] {p : R} (hp : 0 < p) (a b : R) (m : ℕ) [inst_4 : m.AtLeastTwo],
  toIcoMod hp a (b + OfNat.ofNat m * p) = toIcoMod hp a b
-- Mathlib.Analysis.Normed.Unbundled.RingSeminorm
MulRingNorm.funLike : {R : Type u_1} → [inst : NonAssocRing R] → FunLike (MulRingNorm R) R ℝ
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Linear
/-- The composition of `Ext`, as a bilinear map.  -/
CategoryTheory.Abelian.Ext.bilinearCompOfLinear : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      [inst_2 : CategoryTheory.HasExt C] →
        (R : Type t) →
          [inst_3 : CommRing R] →
            [inst_4 : CategoryTheory.Linear R C] →
              (X Y Z : C) →
                (a b c : ℕ) →
                  a + b = c →
                    CategoryTheory.Abelian.Ext X Y a →ₗ[R]
                      CategoryTheory.Abelian.Ext Y Z b →ₗ[R] CategoryTheory.Abelian.Ext X Z c
-- Mathlib.Algebra.Order.Hom.Ring
OrderRingHom.coe_comp : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : NonAssocSemiring α] [inst_1 : Preorder α]
  [inst_2 : NonAssocSemiring β] [inst_3 : Preorder β] [inst_4 : NonAssocSemiring γ] [inst_5 : Preorder γ] (f : β →+*o γ)
  (g : α →+*o β), ⇑(f.comp g) = ⇑f ∘ ⇑g
-- Init.Data.String.Basic
/-- Returns the character at the position `pos` of a string, taking a proof that `p` is not the
past-the-end position.

This function is overridden with an efficient implementation in runtime code.

Examples:
* `("abc".pos ⟨1⟩ (by decide)).get (by decide) = 'b'`
* `("L∃∀N".pos ⟨1⟩ (by decide)).get (by decide) = '∃'`
 -/
String.Pos.get : {s : String} → (pos : s.Pos) → pos ≠ s.endPos → Char
-- Init.Data.Array.Lemmas
Array.flatMap_toArray_cons : ∀ {α : Type u_1} {β : Type u_2} {f : α → Array β} {a : α} {as : List α},
  Array.flatMap f (a :: as).toArray = f a ++ Array.flatMap f as.toArray
-- Lean.Meta.Sym.SymM
Lean.Meta.Sym.ProofInstArgInfo.mk.sizeOf_spec : ∀ (isProof isInstance : Bool),
  sizeOf { isProof := isProof, isInstance := isInstance } = 1 + sizeOf isProof + sizeOf isInstance
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
CFC.eq_one_of_spectrum_subset_one : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : TopologicalSpace A] [inst_6 : Ring A]
  [inst_7 : StarRing A] [inst_8 : Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] (a : A),
  spectrum R a ⊆ {1} → autoParam (p a) CFC.eq_one_of_spectrum_subset_one._auto_1 → a = 1
-- Mathlib.Analysis.Normed.Affine.AddTorsor
nndist_homothety_self : ∀ {V : Type u_1} {P : Type u_2} [inst : SeminormedAddCommGroup V] [inst_1 : PseudoMetricSpace P]
  [inst_2 : NormedAddTorsor V P] {𝕜 : Type u_5} [inst_3 : NormedField 𝕜] [inst_4 : NormedSpace 𝕜 V] (p₁ p₂ : P) (c : 𝕜),
  nndist ((AffineMap.homothety p₁ c) p₂) p₂ = ‖1 - c‖₊ * nndist p₁ p₂
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Square
CategoryTheory.Square.isPushout_iff_op_map_yoneda_isPullback : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C),
  sq.IsPushout ↔ ∀ (X : C), (sq.op.map (CategoryTheory.yoneda.obj X)).IsPullback
-- Mathlib.Analysis.Calculus.BumpFunction.Basic
ContDiff.contDiffBump : ∀ {E : Type u_1} {X : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup X]
  [inst_3 : NormedSpace ℝ X] [inst_4 : HasContDiffBump E] {n : ℕ∞} {c g : X → E} {f : (x : X) → ContDiffBump (c x)},
  ContDiff ℝ (↑n) c →
    (ContDiff ℝ ↑n fun x => (f x).rIn) →
      (ContDiff ℝ ↑n fun x => (f x).rOut) → ContDiff ℝ (↑n) g → ContDiff ℝ ↑n fun x => ↑(f x) (g x)
-- Mathlib.Algebra.Order.ToIntervalMod
iUnion_Ico_zsmul : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [IsOrderedAddMonoid α] [Archimedean α] {p : α},
  0 < p → ⋃ n, Set.Ico (n • p) ((n + 1) • p) = Set.univ