mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.DocString.Types
Lean.Doc.Block.brecOn_3.go : {i : Type u} →
  {b : Type v} →
    {motive_1 : Lean.Doc.Block i b → Sort u_1} →
      {motive_2 : Array (Lean.Doc.ListItem (Lean.Doc.Block i b)) → Sort u_1} →
        {motive_3 : Array (Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b)) → Sort u_1} →
          {motive_4 : Array (Lean.Doc.Block i b) → Sort u_1} →
            {motive_5 : List (Lean.Doc.ListItem (Lean.Doc.Block i b)) → Sort u_1} →
              {motive_6 : List (Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b)) → Sort u_1} →
                {motive_7 : List (Lean.Doc.Block i b) → Sort u_1} →
                  {motive_8 : Lean.Doc.ListItem (Lean.Doc.Block i b) → Sort u_1} →
                    {motive_9 : Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b) → Sort u_1} →
                      (t : Array (Lean.Doc.Block i b)) →
                        ((t : Lean.Doc.Block i b) → t.below → motive_1 t) →
                          ((t : Array (Lean.Doc.ListItem (Lean.Doc.Block i b))) →
                              Lean.Doc.Block.below_1 t → motive_2 t) →
                            ((t : Array (Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b))) →
                                Lean.Doc.Block.below_2 t → motive_3 t) →
                              ((t : Array (Lean.Doc.Block i b)) → Lean.Doc.Block.below_3 t → motive_4 t) →
                                ((t : List (Lean.Doc.ListItem (Lean.Doc.Block i b))) →
                                    Lean.Doc.Block.below_4 t → motive_5 t) →
                                  ((t : List (Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b))) →
                                      Lean.Doc.Block.below_5 t → motive_6 t) →
                                    ((t : List (Lean.Doc.Block i b)) → Lean.Doc.Block.below_6 t → motive_7 t) →
                                      ((t : Lean.Doc.ListItem (Lean.Doc.Block i b)) →
                                          Lean.Doc.Block.below_7 t → motive_8 t) →
                                        ((t : Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b)) →
                                            Lean.Doc.Block.below_8 t → motive_9 t) →
                                          motive_4 t ×' Lean.Doc.Block.below_3 t
-- Mathlib.Data.Nat.Digits.Lemmas
Nat.head!_digits : ∀ {b n : ℕ}, b ≠ 1 → (b.digits n).head! = n % b
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Order
generateFrom_Icc_mem_le_borel : ∀ {α : Type u_5} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderClosedTopology α] (s t : Set α),
  MeasurableSpace.generateFrom {S | ∃ l ∈ s, ∃ u ∈ t, l ≤ u ∧ Set.Icc l u = S} ≤ borel α
-- Mathlib.Analysis.Calculus.Deriv.Comp
HasDerivAtFilter.comp_of_eq : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] (x : 𝕜) {𝕜' : Type u_1} [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {h : 𝕜 → 𝕜'} {h₂ : 𝕜' → 𝕜'} {h' h₂' y : 𝕜'} {L : Filter 𝕜} {L' : Filter 𝕜'},
  HasDerivAtFilter h₂ h₂' (L' ×ˢ pure y) →
    HasDerivAtFilter h h' (L ×ˢ pure x) →
      Filter.Tendsto h L L' → y = h x → HasDerivAtFilter (h₂ ∘ h) (h₂' * h') (L ×ˢ pure x)
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
/-- An oriented angle is unchanged by replacing the first point by one weakly further away on the
same ray.  -/
Wbtw.oangle_eq_left : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {p₁ p₁' p₂ p₃ : P},
  Wbtw ℝ p₂ p₁ p₁' → p₁ ≠ p₂ → EuclideanGeometry.oangle p₁ p₂ p₃ = EuclideanGeometry.oangle p₁' p₂ p₃
-- Mathlib.MeasureTheory.Measure.PreVariation
MeasureTheory.preVariation.zero : ∀ {X : Type u_1} [inst : MeasurableSpace X], MeasureTheory.preVariationFun 0 = 0
-- Mathlib.Data.Num.Lemmas
Num.cast_toZNumNeg : ∀ {α : Type u_1} [inst : SubtractionMonoid α] [inst_1 : One α] (n : Num), ↑n.toZNumNeg = -↑n
-- Mathlib.Order.Filter.Basic
Filter.frequently_or_distrib_right : ∀ {α : Type u} {f : Filter α} [f.NeBot] {p : α → Prop} {q : Prop},
  (∃ᶠ (x : α) in f, p x ∨ q) ↔ (∃ᶠ (x : α) in f, p x) ∨ q
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Add
Std.Tactic.BVDecide.BVExpr.bitblast.FullAdderOutput.mk.congr_simp : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {old : Std.Sat.AIG α} (aig : Std.Sat.AIG α)
  (out out_1 : aig.Ref),
  out = out_1 →
    ∀ (cout cout_1 : aig.Ref),
      cout = cout_1 →
        ∀ (hle : old.decls.size ≤ aig.decls.size),
          { aig := aig, out := out, cout := cout, hle := hle } =
            { aig := aig, out := out_1, cout := cout_1, hle := hle }
-- Mathlib.Algebra.Category.CoalgCat.Monoidal
CoalgCat.rightUnitor_def : ∀ (R : Type u) [inst : CommRing R] (X : CoalgCat R),
  CategoryTheory.MonoidalCategoryStruct.rightUnitor X = (Coalgebra.TensorProduct.rid R R ↑X.toModuleCat).toCoalgIso
-- Mathlib.Order.Hom.Bounded
TopHom.instLE.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : Top α] [inst_1 : LE β] [inst_2 : Top β],
  TopHom.instLE = { le := fun f g => ⇑f ≤ ⇑g }
-- Mathlib.Computability.TuringMachine.ToPartrec
_private.Mathlib.Computability.TuringMachine.ToPartrec.0.Turing.PartrecToTM2.trStmts₁.match_1.eq_5 : ∀ (motive : Turing.PartrecToTM2.Λ' → Sort u_1) (q : Turing.PartrecToTM2.Λ')
  (h_1 :
    (Q : Turing.PartrecToTM2.Λ') →
      (p : Turing.PartrecToTM2.Γ' → Bool) →
        (k₁ k₂ : Turing.PartrecToTM2.K') →
          (q : Turing.PartrecToTM2.Λ') →
            Q = Turing.PartrecToTM2.Λ'.move p k₁ k₂ q → motive (Turing.PartrecToTM2.Λ'.move p k₁ k₂ q))
  (h_2 :
    (Q : Turing.PartrecToTM2.Λ') →
      (k : Turing.PartrecToTM2.K') →
        (s : Option Turing.PartrecToTM2.Γ' → Option Turing.PartrecToTM2.Γ') →
          (q : Turing.PartrecToTM2.Λ') →
            Q = Turing.PartrecToTM2.Λ'.push k s q → motive (Turing.PartrecToTM2.Λ'.push k s q))
  (h_3 :
    (Q : Turing.PartrecToTM2.Λ') →
      (q : Option Turing.PartrecToTM2.Γ' → Turing.PartrecToTM2.Λ') →
        Q = Turing.PartrecToTM2.Λ'.read q → motive (Turing.PartrecToTM2.Λ'.read q))
  (h_4 :
    (Q : Turing.PartrecToTM2.Λ') →
      (p : Turing.PartrecToTM2.Γ' → Bool) →
        (k : Turing.PartrecToTM2.K') →
          (q : Turing.PartrecToTM2.Λ') →
            Q = Turing.PartrecToTM2.Λ'.clear p k q → motive (Turing.PartrecToTM2.Λ'.clear p k q))
  (h_5 : (Q q : Turing.PartrecToTM2.Λ') → Q = q.copy → motive q.copy)
  (h_6 : (Q q : Turing.PartrecToTM2.Λ') → Q = q.succ → motive q.succ)
  (h_7 : (Q q₁ q₂ : Turing.PartrecToTM2.Λ') → Q = q₁.pred q₂ → motive (q₁.pred q₂))
  (h_8 :
    (Q : Turing.PartrecToTM2.Λ') →
      (k : Turing.PartrecToTM2.Cont') → Q = Turing.PartrecToTM2.Λ'.ret k → motive (Turing.PartrecToTM2.Λ'.ret k)),
  (match q.copy with
    | Q@h:(Turing.PartrecToTM2.Λ'.move p k₁ k₂ q) => h_1 Q p k₁ k₂ q h
    | Q@h:(Turing.PartrecToTM2.Λ'.push k s q) => h_2 Q k s q h
    | Q@h:(Turing.PartrecToTM2.Λ'.read q) => h_3 Q q h
    | Q@h:(Turing.PartrecToTM2.Λ'.clear p k q) => h_4 Q p k q h
    | Q@h:q.copy => h_5 Q q h
    | Q@h:q.succ => h_6 Q q h
    | Q@h:(q₁.pred q₂) => h_7 Q q₁ q₂ h
    | Q@h:(Turing.PartrecToTM2.Λ'.ret k) => h_8 Q k h) =
    h_5 q.copy q ⋯
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.maxKey?_eq_some_maxKey! : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α], t ≠ ∅ → t.maxKey? = some t.maxKey!
-- Lean.Message
Lean.MessageData.isTrace : Lean.MessageData → Bool
-- Mathlib.Logic.Basic
Iff.ne_right : ∀ {α : Sort u_1} {β : Sort u_2} {a b : α} {c d : β}, (a ≠ b ↔ c = d) → (a = b ↔ c ≠ d)
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
NumberField.place_apply : ∀ {K : Type u_1} [inst : Field K] {A : Type u_2} [inst_1 : NormedDivisionRing A] (φ : K →+* A) (x : K),
  (NumberField.place φ) x = ‖φ x‖
-- Mathlib.Analysis.SumOverResidueClass
/-- A decreasing sequence of real numbers is summable on a residue class
if and only if it is summable.  -/
summable_indicator_mod_iff : ∀ {m : ℕ} [NeZero m] {f : ℕ → ℝ}, Antitone f → ∀ (k : ZMod m), Summable ({n | ↑n = k}.indicator f) ↔ Summable f
-- Mathlib.RingTheory.Polynomial.Basic
MvPolynomial.ker_map : ∀ {R : Type u} {S : Type u_1} {σ : Type v} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
  RingHom.ker (MvPolynomial.map f) = Ideal.map MvPolynomial.C (RingHom.ker f)
-- Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
/-- `X.skeleton n` is the subcomplex of `X` generated by (non-degenerate)
simplices of dimension `< n`.  -/
SSet.skeleton : (X : SSet) → ℕ →o X.Subcomplex
-- Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject
CategoryTheory.SimplicialObject.Splitting.σ_comp_πSummand_id_eq_zero_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : CategoryTheory.SimplicialObject C} (s : X.Splitting)
  [inst_1 : CategoryTheory.Preadditive C] {n : ℕ} (i : Fin (n + 1)) {Z : C}
  (h :
    s.N (Opposite.unop (CategoryTheory.SimplicialObject.Splitting.IndexSet.id (Opposite.op { len := n + 1 })).fst).len ⟶
      Z),
  CategoryTheory.CategoryStruct.comp (X.σ i)
      (CategoryTheory.CategoryStruct.comp
        (s.πSummand (CategoryTheory.SimplicialObject.Splitting.IndexSet.id (Opposite.op { len := n + 1 }))) h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Mathlib.Algebra.Order.PUnit
PUnit.isOrderedCancelAddMonoid : IsOrderedCancelAddMonoid PUnit.{u_1 + 1}
-- Std.Http.Protocol.H1
Std.Http.Protocol.H1.StepResult.mk.injEq : ∀ {dir : Std.Http.Protocol.H1.Direction} (events : Array (Std.Http.Protocol.H1.Event dir))
  (output : Std.Http.Internal.ChunkedBuffer) (events_1 : Array (Std.Http.Protocol.H1.Event dir))
  (output_1 : Std.Http.Internal.ChunkedBuffer),
  ({ events := events, output := output } = { events := events_1, output := output_1 }) =
    (events = events_1 ∧ output = output_1)
-- Mathlib.Analysis.Distribution.SchwartzSpace.Deriv
/-- Integration by parts of Schwartz functions for the Laplacian.

Version for multiplication of scalar-valued Schwartz functions.  -/
SchwartzMap.integral_mul_laplacian_right_eq_left : ∀ {𝕜 : Type u_2} {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E]
  [inst_2 : FiniteDimensional ℝ E] [inst_3 : MeasurableSpace E] {μ : MeasureTheory.Measure E} [BorelSpace E]
  [μ.IsAddHaarMeasure] [inst_6 : NormedRing 𝕜] [inst_7 : NormedSpace ℝ 𝕜] [IsScalarTower ℝ 𝕜 𝕜] [SMulCommClass ℝ 𝕜 𝕜]
  (f g : SchwartzMap E 𝕜), ∫ (x : E), f x * (Laplacian.laplacian g) x ∂μ = ∫ (x : E), (Laplacian.laplacian f) x * g x ∂μ
-- Std.Http.Protocol.H1.Writer
/-- Writing a chunked transfer-encoding body (HTTP/1.1).
 -/
Std.Http.Protocol.H1.Writer.State.writingBodyChunked : Std.Http.Protocol.H1.Writer.State
-- Mathlib.Algebra.Group.Equiv.Defs
MulEquiv.symm_comp_self : ∀ {M : Type u_4} {N : Type u_5} [inst : Mul M] [inst_1 : Mul N] (e : M ≃* N), ⇑e.symm ∘ ⇑e = id
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mod
CategoryTheory.ModObj.leftSMul_fst_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] {M : C}
  [inst_2 : CategoryTheory.MonObj M] {X : C} [inst_3 : CategoryTheory.ModObj M X] {Z : C} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.ModObj.leftSMul M X)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.fst X X) h) =
    CategoryTheory.CategoryStruct.comp CategoryTheory.ModObj.smul h
-- Mathlib.Analysis.SpecialFunctions.Sigmoid
unitInterval.sigmoid_neg : ∀ (x : ℝ), unitInterval.sigmoid (-x) = unitInterval.symm (unitInterval.sigmoid x)
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
/-- A chosen left Kan extension when `[HasLeftKanExtension L F]` holds.  -/
CategoryTheory.Functor.leftKanExtension : {C : Type u_1} →
  {H : Type u_3} →
    {D : Type u_4} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_3, u_3} H] →
          [inst_2 : CategoryTheory.Category.{v_4, u_4} D] →
            (L : CategoryTheory.Functor C D) →
              (F : CategoryTheory.Functor C H) → [L.HasLeftKanExtension F] → CategoryTheory.Functor D H
-- Lean.Meta.IndPredBelow
_private.Lean.Meta.IndPredBelow.0.Lean.Meta.IndPredBelow.mkBRecOn : Lean.Meta.IndPredBelow.Context✝ → Lean.MetaM Unit
-- Mathlib.Analysis.Complex.Exponential
Complex.exp_ofReal_im : ∀ (x : ℝ), (Complex.exp ↑x).im = 0
-- Mathlib.Analysis.Convex.Deriv
ConcaveOn.le_slope_of_hasDerivWithinAt : ∀ {S : Set ℝ} {f : ℝ → ℝ} {x y f' : ℝ},
  ConcaveOn ℝ S f → x ∈ S → y ∈ S → x < y → HasDerivWithinAt f f' S y → f' ≤ slope f x y
-- Lean.Elab.PreDefinition.WF.GuessLex
Lean.Elab.WF.GuessLex.SavedLocalContext.savedState : Lean.Elab.WF.GuessLex.SavedLocalContext → Lean.Meta.SavedState
-- Mathlib.RingTheory.Congruence.Defs
RingCon.coe_sub : ∀ {R : Type u_1} [inst : AddGroup R] [inst_1 : Mul R] (c : RingCon R) (x y : R), ↑(x - y) = ↑x - ↑y
-- Mathlib.Order.Filter.Pointwise
Filter.neg_le_neg_iff : ∀ {α : Type u_2} [inst : InvolutiveNeg α] {f g : Filter α}, -f ≤ -g ↔ f ≤ g
-- Lean.Util.Heartbeats
/-- Returns the current `initHeartbeats`.  -/
Lean.getInitHeartbeats : Lean.CoreM ℕ
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
CategoryTheory.Presieve.CoverByImageStructure.lift : {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] →
        {G : CategoryTheory.Functor C D} →
          {V U : D} → {f : V ⟶ U} → (self : CategoryTheory.Presieve.CoverByImageStructure G f) → V ⟶ G.obj self.obj
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
AddHom.withTopMap_apply : ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] (f : M →ₙ+ N), ⇑f.withTopMap = WithTop.map ⇑f
-- Mathlib.Topology.Irreducible
Homeomorph.irreducibleSpace_iff : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (e : X ≃ₜ Y),
  IrreducibleSpace X ↔ IrreducibleSpace Y
-- Mathlib.Algebra.Module.Submodule.LinearMap
Submodule.inclusion_apply : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {p p' : Submodule R M} (h : p ≤ p') (x : ↥p), (Submodule.inclusion h) x = ⟨↑x, ⋯⟩
-- Mathlib.Analysis.Complex.Trigonometric
Complex.cosh_three_mul : ∀ (x : ℂ), Complex.cosh (3 * x) = 4 * Complex.cosh x ^ 3 - 3 * Complex.cosh x
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.foldrM.eq_2 : ∀ {α : Type u} {β : α → Type v} {δ : Type w} {m : Type w → Type u_1} [inst : Monad m] (f : (a : α) → β a → δ → m δ)
  (init : δ) (size : ℕ) (k' : α) (v : β k') (l r : Std.DTreeMap.Internal.Impl α β),
  Std.DTreeMap.Internal.Impl.foldrM f init (Std.DTreeMap.Internal.Impl.inner size k' v l r) = do
    let right ← Std.DTreeMap.Internal.Impl.foldrM f init r
    let middle ← f k' v right
    Std.DTreeMap.Internal.Impl.foldrM f middle l
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.uniqueRingEquiv.congr_simp : ∀ {R : Type u_1} (M : Type u_4) [inst : Semiring R] [inst_1 : Monoid M] [inst_2 : Subsingleton M],
  MonoidAlgebra.uniqueRingEquiv M = MonoidAlgebra.uniqueRingEquiv M
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.CategoryWithHomology.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C],
  (∀ (S : CategoryTheory.ShortComplex C), S.HasHomology) → CategoryTheory.CategoryWithHomology C
-- Mathlib.Analysis.Normed.Lp.WithLp
WithLp.equiv_apply : ∀ (p : ENNReal) (V : Type u_4) (self : WithLp p V), (WithLp.equiv p V) self = self.ofLp
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.Cont.eval.eq_5 : ∀ (f : Turing.ToPartrec.Code) (k : Turing.ToPartrec.Cont),
  (Turing.ToPartrec.Cont.fix f k).eval = fun v => if v.headI = 0 then k.eval v.tail else f.fix.eval v.tail >>= k.eval
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.Nonempty.zpow : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : DivisionMonoid α] {s : Finset α},
  s.Nonempty → ∀ {n : ℤ}, (s ^ n).Nonempty
-- Lean.Message
Lean.instFromJsonMessageSeverity.fromJson : Lean.Json → Except String Lean.MessageSeverity
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.pullbackProdFstIsoProd_inv_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) (Z : C)
  [inst_1 : CategoryTheory.Limits.HasBinaryProduct Y Z] [inst_2 : CategoryTheory.Limits.HasBinaryProduct X Z]
  [inst_3 : CategoryTheory.Limits.HasPullback f CategoryTheory.Limits.prod.fst],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackProdFstIsoProd f Z).inv
      (CategoryTheory.Limits.pullback.fst f CategoryTheory.Limits.prod.fst) =
    CategoryTheory.Limits.prod.fst
-- Mathlib.CategoryTheory.Opposites
/-- The functor from the double-opposite of a category to the underlying category.  -/
CategoryTheory.unopUnop : (C : Type u₁) → [inst : CategoryTheory.Category.{v₁, u₁} C] → CategoryTheory.Functor Cᵒᵖᵒᵖ C
-- Mathlib.Computability.Reduce
ManyOneDegree.liftOn₂_eq : ∀ {φ : Sort u_1} (p q : Set ℕ) (f : Set ℕ → Set ℕ → φ)
  (h : ∀ (p₁ p₂ q₁ q₂ : ℕ → Prop), ManyOneEquiv p₁ p₂ → ManyOneEquiv q₁ q₂ → f p₁ q₁ = f p₂ q₂),
  (ManyOneDegree.of p).liftOn₂ (ManyOneDegree.of q) f h = f p q
-- Mathlib.Analysis.Normed.Algebra.Spectrum
spectrum.isBounded : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NormedField 𝕜] [inst_1 : NormedRing A] [inst_2 : NormedAlgebra 𝕜 A]
  [CompleteSpace A] (a : A), Bornology.IsBounded (spectrum 𝕜 a)
-- Mathlib.Data.TypeVec
/-- specialized cases distinction for an arrow in the category of (n+1)-length type vectors  -/
TypeVec.typevecCasesCons₂ : (n : ℕ) →
  (t : Type u_1) →
    (t' : Type u_2) →
      (v : TypeVec.{u_1} n) →
        (v' : TypeVec.{u_2} n) →
          {β : (v ::: t).Arrow (v' ::: t') → Sort u_3} →
            ((f : t → t') → (fs : v.Arrow v') → β (fs ::: f)) → (fs : (v ::: t).Arrow (v' ::: t')) → β fs
-- Mathlib.Algebra.Lie.Nilpotent
LieModule.instIsNilpotentTensor : ∀ (R : Type u_1) (A : Type u_2) (L : Type u_3) (M : Type u_4) [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : LieAlgebra R L] [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M]
  [inst_6 : LieModule R L M] [inst_7 : CommRing A] [inst_8 : Algebra R A] [LieModule.IsNilpotent L M],
  LieModule.IsNilpotent (TensorProduct R A L) (TensorProduct R A M)
-- Mathlib.AlgebraicTopology.SimplicialSet.RelativeMorphism
/-- The homotopy class of a relative morphism.  -/
SSet.RelativeMorphism.homotopyClass : {X Y : SSet} →
  {A : X.Subcomplex} →
    {B : Y.Subcomplex} →
      {φ : A.toSSet ⟶ B.toSSet} → SSet.RelativeMorphism A B φ → SSet.RelativeMorphism.HomotopyClass A B φ
-- Mathlib.Algebra.Module.Equiv.Basic
LinearEquiv.zero_apply : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {σ₁₂ : R →+* R₂}
  {σ₂₁ : R₂ →+* R} [inst_6 : RingHomInvPair σ₁₂ σ₂₁] [inst_7 : RingHomInvPair σ₂₁ σ₁₂] [inst_8 : Subsingleton M]
  [inst_9 : Subsingleton M₂] (x : M), 0 x = 0
-- Mathlib.Data.List.Sort
/-- **Alias** of the reverse direction of `List.sortedGT_reverse`. -/
List.SortedLT.reverse : ∀ {α : Type u_1} {l : List α} [inst : Preorder α], l.SortedLT → l.reverse.SortedGT
-- Mathlib.Topology.Constructible
/-- A set in a topological space is locally constructible, if every point has a neighborhood on
which the set is constructible.  -/
Topology.IsLocallyConstructible : {X : Type u_2} → [TopologicalSpace X] → Set X → Prop
-- Mathlib.CategoryTheory.ShrinkYoneda
CategoryTheory.shrinkYonedaIsoYoneda_inv_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : C),
  CategoryTheory.shrinkYonedaIsoYoneda.inv.app X =
    (CategoryTheory.NatIso.ofComponents (fun Y => CategoryTheory.shrinkYonedaObjObjEquiv.toIso) ⋯).inv
-- Init.Data.List.Impl
List.filterMapTR.go.eq_def : ∀ {α : Type u_1} {β : Type u_2} (f : α → Option β) (a : List α) (a_1 : Array β),
  List.filterMapTR.go f a a_1 =
    match a, a_1 with
    | [], acc => acc.toList
    | a :: as, acc =>
      match f a with
      | none => List.filterMapTR.go f as acc
      | some b => List.filterMapTR.go f as (acc.push b)
-- Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
/-- Given natural transformations `F ⟶ F₁` and `F ⟶ F₂`, construct
a natural transformation `F ⟶ prod F₁ F₂`.  -/
CategoryTheory.FunctorToTypes.prod.lift : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F F₁ F₂ : CategoryTheory.Functor C (Type w)} → (F ⟶ F₁) → (F ⟶ F₂) → (F ⟶ CategoryTheory.FunctorToTypes.prod F₁ F₂)
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Real
/-- A limit (over a general filter) of a.e.-measurable `ℝ≥0∞`-valued functions is
a.e.-measurable.  -/
ENNReal.aemeasurable_of_tendsto' : ∀ {α : Type u_1} {mα : MeasurableSpace α} {ι : Type u_5} {f : ι → α → ENNReal} {g : α → ENNReal}
  {μ : MeasureTheory.Measure α} (u : Filter ι) [u.NeBot] [u.IsCountablyGenerated],
  (∀ (i : ι), AEMeasurable (f i) μ) → (∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun i => f i a) u (nhds (g a))) → AEMeasurable g μ
-- Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
/-- The limit of `(1 + g n) ^ n` as `(n : ℝ) → ∞` is `exp t`,
where `t : ℝ` is the limit of `n * g n`.  -/
Real.tendsto_one_add_pow_exp_of_tendsto : ∀ {g : ℕ → ℝ} {t : ℝ},
  Filter.Tendsto (fun n => ↑n * g n) Filter.atTop (nhds t) →
    Filter.Tendsto (fun n => (1 + g n) ^ n) Filter.atTop (nhds (Real.exp t))
-- Mathlib.RingTheory.DedekindDomain.Instances
instIsTorsionFreeLocalizationAlgebraMapSubmonoidPrimeCompl_2 : ∀ {R : Type u_1} (S : Type u_2) (T : Type u_3) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  [IsDomain R] [IsDomain S] [IsDomain T] [inst_6 : Algebra R S] {P : Ideal R} [inst_7 : P.IsPrime] [FaithfulSMul R S]
  [inst_9 : Algebra S T] [inst_10 : Algebra R T] [inst_11 : IsScalarTower R S T] [Module.IsTorsionFree S T],
  Module.IsTorsionFree (Localization (Algebra.algebraMapSubmonoid S P.primeCompl))
    (Localization (Algebra.algebraMapSubmonoid T P.primeCompl))
-- Mathlib.Probability.Kernel.Defs
ProbabilityTheory.Kernel.instFunLike : {α : Type u_1} →
  {β : Type u_2} →
    {mα : MeasurableSpace α} →
      {mβ : MeasurableSpace β} → FunLike (ProbabilityTheory.Kernel α β) α (MeasureTheory.Measure β)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.get!_diff_of_not_mem_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited β], m₁.WF → m₂.WF → ∀ {k : α}, k ∉ m₂ → (m₁ \ m₂).get! k = m₁.get! k
-- Mathlib.Algebra.Homology.Embedding.CochainComplex
CochainComplex.isZero_of_isLE : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : CochainComplex C ℤ) (n i : ℤ),
  autoParam (n < i) CochainComplex.isZero_of_isLE._auto_1 →
    ∀ [K.IsLE n] [inst_3 : HomologicalComplex.HasHomology K i],
      CategoryTheory.Limits.IsZero (HomologicalComplex.homology K i)
-- Mathlib.RingTheory.MvPowerSeries.Restricted
MvPowerSeries.isRestricted.add : ∀ {R : Type u_1} [inst : NormedRing R] {σ : Type u_2} (c : σ → ℝ) {f g : MvPowerSeries σ R},
  MvPowerSeries.IsRestricted c f → MvPowerSeries.IsRestricted c g → MvPowerSeries.IsRestricted c (f + g)
-- Mathlib.Data.Fin.Embedding
Fin.succAboveEmb_apply : ∀ {n : ℕ} (p : Fin (n + 1)) (i : Fin n), p.succAboveEmb i = p.succAbove i
-- Mathlib.Topology.Algebra.StarSubalgebra
StarAlgebra.elemental.starAlgHomClass_ext : ∀ (R : Type u_1) {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R]
  [inst_2 : TopologicalSpace A] [inst_3 : Semiring A] [inst_4 : StarRing A] [inst_5 : IsSemitopologicalSemiring A]
  [inst_6 : ContinuousStar A] [inst_7 : Algebra R A] [inst_8 : StarModule R A] [inst_9 : TopologicalSpace B]
  [inst_10 : Semiring B] [inst_11 : StarRing B] [inst_12 : Algebra R B] [T2Space B] {F : Type u_4} {a : A}
  [inst_14 : FunLike F (↥(StarAlgebra.elemental R a)) B] [AlgHomClass F R (↥(StarAlgebra.elemental R a)) B]
  [StarHomClass F (↥(StarAlgebra.elemental R a)) B] {φ ψ : F},
  Continuous ⇑φ → Continuous ⇑ψ → φ ⟨a, ⋯⟩ = ψ ⟨a, ⋯⟩ → φ = ψ
-- Mathlib.Algebra.Notation.Prod
Prod.snd_mul : ∀ {M : Type u_8} {N : Type u_9} [inst : Mul M] [inst_1 : Mul N] (p q : M × N), (p * q).2 = p.2 * q.2