mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
/-- Reversing the order of the points passed to `oangle` negates the angle.  -/
EuclideanGeometry.oangle_rev : ∀ {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), EuclideanGeometry.oangle p₃ p₂ p₁ = -EuclideanGeometry.oangle p₁ p₂ p₃
-- Mathlib.Order.Defs.Unbundled
trans_of : ∀ {α : Sort u_1} (r : α → α → Prop) {a b c : α} [IsTrans α r], r a b → r b c → r a c
-- Lean.Parser.Command
Lean.Parser.Command.optDeclSig.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Order.Category.HeytAlg
HeytAlg.hasForgetToLat_forget₂_obj_carrier : ∀ (X : HeytAlg), ↑(CategoryTheory.HasForget₂.forget₂.obj X).toDistLat = ↑X
-- Mathlib.Combinatorics.Enumerative.Catalan.Basic
_private.Mathlib.Combinatorics.Enumerative.Catalan.Basic.0.gosper_trick : ∀ {n i : ℕ},
  i ≤ n →
    gosperCatalan✝ (n + 1) (i + 1) - gosperCatalan✝ (n + 1) i =
      ↑i.centralBinom / (↑i + 1) * ↑(n - i).centralBinom / (↑n - ↑i + 1)
-- Init.Data.String.Iterate
/-- Folds a function over a slice from the end, accumulating a value starting with `init`. The
accumulated value is combined with each character in reverse order, using `f`.

Examples:

* `"coffee tea water".toSlice.foldr (fun c n => if c.isWhitespace then n + 1 else n) 0 = 2`

* `"coffee tea and water".toSlice.foldr (fun c n => if c.isWhitespace then n + 1 else n) 0 = 3`

* `"coffee tea water".toSlice.foldr (fun c s => s.push c) "" = "retaw aet eeffoc"`
 -/
String.Slice.foldr : {α : Type u} → (Char → α → α) → α → String.Slice → α
-- Mathlib.NumberTheory.LSeries.Linearity
LSeriesHasSum.sub : ∀ {f g : ℕ → ℂ} {s a b : ℂ}, LSeriesHasSum f s a → LSeriesHasSum g s b → LSeriesHasSum (f - g) s (a - b)
-- Init.Data.List.Lemmas
List.mem_of_getElem : ∀ {α : Type u_1} {l : List α} {i : ℕ} {h : i < l.length} {a : α}, l[i] = a → a ∈ l
-- Mathlib.Analysis.Calculus.TangentCone.Basic
uniqueDiffWithinAt_inter : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Semiring 𝕜] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] [ContinuousAdd E] {s t : Set E} {x : E},
  t ∈ nhds x → (UniqueDiffWithinAt 𝕜 (s ∩ t) x ↔ UniqueDiffWithinAt 𝕜 s x)
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.mk.congr_simp : ∀ {V : Type u} (Adj Adj_1 : V → V → Prop) (e_Adj : Adj = Adj_1) (symm : Std.Symm Adj) (loopless : Std.Irrefl Adj),
  { Adj := Adj, symm := symm, loopless := loopless } = { Adj := Adj_1, symm := ⋯, loopless := ⋯ }
-- Mathlib.Algebra.Algebra.NonUnitalHom
NonUnitalAlgHom.coe_inr : ∀ {R : Type u} [inst : Monoid R] {A : Type v} {B : Type w} [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : DistribMulAction R A] [inst_3 : NonUnitalNonAssocSemiring B] [inst_4 : DistribMulAction R B],
  ⇑(NonUnitalAlgHom.inr R A B) = Prod.mk 0
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Lemmas
/-- This invariant states that if the `assignments` field of a default formula `f` indicates that `f`
contains an assignment `b` at index `i`, then the unit literal `(i, b)` must be included in `f`.
Default formulas are expected to satisfy this invariant at all times except during intermediate
stages of unit propagation (during which, default formulas are only expected to satisfy the more
lenient `AssignmentsInvariant` defined below).
 -/
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.StrongAssignmentsInvariant : {n : ℕ} → Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n → Prop
-- Mathlib.Data.Sym.Sym2
Sym2.IsDiag.map : ∀ {α : Type u_1} {β : Type u_2} {z : Sym2 α} {f : α → β}, z.IsDiag → (Sym2.map f z).IsDiag
-- Std.Data.DHashMap.Internal.Model
Std.DHashMap.Internal.Raw₀.Const.get!_eq_get!ₘ : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : Inhabited β]
  (m : Std.DHashMap.Internal.Raw₀ α fun x => β) (a : α),
  Std.DHashMap.Internal.Raw₀.Const.get! m a = Std.DHashMap.Internal.Raw₀.Const.get!ₘ m a
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.eLpNorm_mono_enorm : ∀ {α : Type u_1} {ε : Type u_2} {ε' : Type u_3} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : ENorm ε] [inst_1 : ENorm ε'] {f : α → ε} {g : α → ε'},
  (∀ (x : α), ‖f x‖ₑ ≤ ‖g x‖ₑ) → MeasureTheory.eLpNorm f p μ ≤ MeasureTheory.eLpNorm g p μ
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.get_erase : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k a : α} {h' : a ∈ t.erase k}, (t.erase k).get a h' = t.get a ⋯
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
Sigma.instMeasurableSpace : {α : Type u_7} → {β : α → Type u_6} → [m : (a : α) → MeasurableSpace (β a)] → MeasurableSpace (Sigma β)
-- Init.Data.List.Sublist
List.subset_append_of_subset_left : ∀ {α : Type u_1} {l l₁ : List α} (l₂ : List α), l ⊆ l₁ → l ⊆ l₁ ++ l₂
-- Std.Data.DTreeMap.Basic
/-- Tries to retrieve the key-value pair with the largest key in the tree map, returning `none` if the
map is empty.
 -/
Std.DTreeMap.maxEntry? : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → Std.DTreeMap α β cmp → Option ((a : α) × β a)
-- Mathlib.Order.SupIndep
Finset.SupIndep.eq_1 : ∀ {α : Type u_1} {ι : Type u_3} [inst : Lattice α] [inst_1 : OrderBot α] (s : Finset ι) (f : ι → α),
  s.SupIndep f = ∀ ⦃t : Finset ι⦄, t ⊆ s → ∀ ⦃i : ι⦄, i ∈ s → i ∉ t → Disjoint (f i) (t.sup f)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.getKeyGTD_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  {k fallback : α}, t₁.Equiv t₂ → t₁.getKeyGTD k fallback = t₂.getKeyGTD k fallback
-- Mathlib.LinearAlgebra.Span.Defs
/-- Unexpander for `R ∙ x` notation. This needs to be defined separately because the `{_}`
notation is ambiguous, so we have to specify that it is the `«term{_}»` notation.  -/
Submodule.span.unexpander : Lean.PrettyPrinter.Unexpander
-- Std.Async.ContextAsync
Std.Async.ContextAsync.instInhabited : {α : Type} → [Inhabited α] → Inhabited (Std.Async.ContextAsync α)
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.archimdeanClassMk_coe : ∀ {x : ℝ}, x ≠ 0 → ArchimedeanClass.mk ↑x = 0
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.LitValue.usize.sizeOf_spec : ∀ (val : UInt64), sizeOf (Lean.Compiler.LCNF.LitValue.usize val) = 1 + sizeOf val
-- Mathlib.Algebra.Order.Group.OrderIso
le_inv' : ∀ {α : Type u} [inst : Group α] [inst_1 : LE α] [MulLeftMono α] [MulRightMono α] {a b : α}, a ≤ b⁻¹ ↔ b ≤ a⁻¹
-- Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
UpperHalfPlane.contMDiff_denom : ∀ {n : WithTop ℕ∞} (g : GL (Fin 2) ℝ),
  ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) n fun τ => UpperHalfPlane.denom g ↑τ
-- Mathlib.Topology.VectorBundle.Basic
VectorBundle.trivialization_linear' : ∀ {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B → Type u_4} {inst : NontriviallyNormedField R}
  {inst_1 : (x : B) → AddCommMonoid (E x)} {inst_2 : (x : B) → Module R (E x)} {inst_3 : NormedAddCommGroup F}
  {inst_4 : NormedSpace R F} {inst_5 : TopologicalSpace B} {inst_6 : TopologicalSpace (Bundle.TotalSpace F E)}
  {inst_7 : (x : B) → TopologicalSpace (E x)} {inst_8 : FiberBundle F E} [self : VectorBundle R F E]
  (e : Bundle.Trivialization F Bundle.TotalSpace.proj) [MemTrivializationAtlas e], Bundle.Trivialization.IsLinear R e
-- Mathlib.MeasureTheory.Measure.MeasureSpaceDef
aemeasurable_id : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}, AEMeasurable id μ
-- Mathlib.AlgebraicGeometry.Sites.EtalePoint
AlgebraicGeometry.Scheme.Etale.mk.congr_simp : ∀ {X Y : AlgebraicGeometry.Scheme} (f f_1 : Y ⟶ X) (e_f : f = f_1) [inst : AlgebraicGeometry.Etale f],
  AlgebraicGeometry.Scheme.Etale.mk f = AlgebraicGeometry.Scheme.Etale.mk f_1
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.InfinitePlace.nrRealPlaces.eq_1 : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  NumberField.InfinitePlace.nrRealPlaces K = Fintype.card { w // w.IsReal }
-- Init.Data.Slice.Array.Lemmas
Array.mkSlice_ric_eq_mkSlice_rco : ∀ {α : Type u_1} {xs : Array α} {hi : ℕ},
  (Std.Ric.Sliceable.mkSlice xs *...=hi) = Std.Rco.Sliceable.mkSlice xs 0...hi + 1
-- Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
LinearEquiv.AssociatedPrimes.eq : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {M' : Type u_3}
  [inst_3 : AddCommMonoid M'] [inst_4 : Module R M'] (l : M ≃ₗ[R] M'), associatedPrimes R M = associatedPrimes R M'
-- Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
/-- A linear independent finset of `finrank K V`-many vectors forms a basis.  -/
finsetBasisOfLinearIndependentOfCardEqFinrank : {K : Type u} →
  {V : Type v} →
    [inst : DivisionRing K] →
      [inst_1 : AddCommGroup V] →
        [inst_2 : Module K V] →
          {s : Finset V} →
            s.Nonempty → LinearIndependent K Subtype.val → s.card = Module.finrank K V → Module.Basis (↥s) K V
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.size_le_size_insertIfNew : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {k : α} {v : β}, m.size ≤ (m.insertIfNew k v).size
-- Lean.Elab.PreDefinition.WF.Basic
Lean.Elab.WF.applyCleanWfTactic : Lean.Elab.Tactic.TacticM Unit
-- Mathlib.Analysis.SpecialFunctions.Stirling
/-- Stirling's approximation gives a lower bound for `log n!` for all positive `n`.
The left-hand side is formulated in decreasing order in `n`: the higher order terms are first.
This is a consequence of `le_factorial_stirling`, but is stated separately since the logarithmic
version is sometimes more practical, and having this version eases algebraic calculations for
applications.
See also `log_stirlingSeq_sdiff_le` for Robbins' sharp bound of `1/(12k(k+1))` on successive
differences in the Stirling sequence, which provides finer control over the convergence rate.
 -/
Stirling.le_log_factorial_stirling : ∀ {n : ℕ}, n ≠ 0 → ↑n * Real.log ↑n - ↑n + Real.log ↑n / 2 + Real.log (2 * Real.pi) / 2 ≤ Real.log ↑n.factorial
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr
Std.Tactic.BVDecide.BVExpr.bitblast.go : {w : ℕ} →
  (aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit) →
    Std.Tactic.BVDecide.BVExpr w → Std.Tactic.BVDecide.BVExpr.Cache aig → Std.Tactic.BVDecide.BVExpr.Return aig w
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
AlgebraicGeometry.Scheme.IdealSheafData.instIsPreimmersionGlueDataObjι : ∀ {X : AlgebraicGeometry.Scheme} (I : X.IdealSheafData) (U : ↑X.affineOpens),
  AlgebraicGeometry.IsPreimmersion (I.glueDataObjι U)
-- Mathlib.Order.SuccPred.Archimedean
monotoneOn_of_pred_le : ∀ {α : Type u_3} {β : Type u_4} [inst : PartialOrder α] [inst_1 : Preorder β] [inst_2 : PredOrder α]
  [IsPredArchimedean α] {s : Set α} {f : α → β},
  s.OrdConnected → (∀ (a : α), ¬IsMin a → a ∈ s → Order.pred a ∈ s → f (Order.pred a) ≤ f a) → MonotoneOn f s
-- Mathlib.NumberTheory.Padics.Complex
/-- The `ℝ≥0`-valued norm on `ℂ_[p]` extends that on `PadicAlgCl p`.  -/
PadicComplex.nnnorm_extends : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] (x : PadicAlgCl p), ‖↑x‖₊ = ‖x‖₊
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.add_one_eq : ∀ {a : Cardinal.{u_1}}, Cardinal.aleph0 ≤ a → a + 1 = a
-- Mathlib.RingTheory.Ideal.Pure
/-- [Stacks Tag 04PS](https://stacks.math.columbia.edu/tag/04PS) ((3) => (1)) -/
Ideal.Pure.of_inf_eq_mul : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R), (∀ ⦃J : Ideal R⦄, J.FG → I ⊓ J = I * J) → I.Pure
-- Mathlib.Analysis.SpecialFunctions.SmoothTransition
/-- The function `expNegInvGlue` is smooth.  -/
expNegInvGlue.contDiff : ∀ {n : ℕ∞}, ContDiff ℝ (↑n) expNegInvGlue
-- Mathlib.AlgebraicGeometry.ColimitsOver
AlgebraicGeometry.Scheme.Cover.ColimitGluingData.transitionMap_comp : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [inst : P.IsStableUnderBaseChange]
  [inst_1 : P.IsMultiplicative] {S : AlgebraicGeometry.Scheme} {J : Type u_1}
  [inst_2 : CategoryTheory.Category.{v_1, u_1} J] {D : CategoryTheory.Functor J (P.Over ⊤ S)} {𝒰 : S.OpenCover}
  [inst_3 : CategoryTheory.Category.{v_2, u_2} 𝒰.I₀] [inst_4 : AlgebraicGeometry.Scheme.Cover.LocallyDirected 𝒰]
  (d : AlgebraicGeometry.Scheme.Cover.ColimitGluingData D 𝒰) {i j k : 𝒰.I₀} (hij : i ⟶ j) (hjk : j ⟶ k),
  d.transitionMap (CategoryTheory.CategoryStruct.comp hij hjk) =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.MorphismProperty.Over.mapComp ⊤ ⋯ ⋯
              (AlgebraicGeometry.Scheme.Cover.trans 𝒰 (CategoryTheory.CategoryStruct.comp hij hjk)) ⋯).hom.app
        (d.cocone i).pt)
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.MorphismProperty.Over.map ⊤ ⋯).map (d.transitionMap hij))
        (d.transitionMap hjk))
-- Mathlib.RingTheory.FractionalIdeal.Basic
FractionalIdeal.mem_coeSubmodule : ∀ {R : Type u_1} [inst : CommRing R] {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P] {x : P} {I : Ideal R},
  x ∈ IsLocalization.coeSubmodule P I ↔ ∃ x' ∈ I, (algebraMap R P) x' = x
-- Std.Data.Internal.List.Associative
Std.Internal.List.DistinctKeys.nil : ∀ {α : Type u} {β : α → Type v} [inst : BEq α], Std.Internal.List.DistinctKeys []
-- Mathlib.Combinatorics.SimpleGraph.Girth
SimpleGraph.Iso.egirth_eq : ∀ {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {G' : SimpleGraph β} (f : G ≃g G'), G.egirth = G'.egirth
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientGroup.congr.eq_1 : ∀ {G : Type u_1} {H : Type u_2} [inst : Group G] [inst_1 : Group H] (G' : Subgroup G) (H' : Subgroup H)
  [inst_2 : G'.Normal] [inst_3 : H'.Normal] (e : G ≃* H) (he : Subgroup.map (↑e) G' = H'),
  QuotientGroup.congr G' H' e he =
    { toFun := ⇑(QuotientGroup.map G' H' ↑e ⋯), invFun := ⇑(QuotientGroup.map H' G' ↑e.symm ⋯), left_inv := ⋯,
      right_inv := ⋯, map_mul' := ⋯ }
-- Mathlib.CategoryTheory.Comma.Arrow
CategoryTheory.Arrow.comp_left : ∀ {T : Type u} [inst : CategoryTheory.Category.{v, u} T] {X Y Z : CategoryTheory.Arrow T} (f : X ⟶ Y) (g : Y ⟶ Z),
  CategoryTheory.Arrow.Hom.left (CategoryTheory.CategoryStruct.comp f g) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.left f) (CategoryTheory.Arrow.Hom.left g)
-- Mathlib.Algebra.Lie.Solvable
/-- The derived series of Lie ideals of a Lie algebra.  -/
LieAlgebra.derivedSeries : (R : Type u) → (L : Type v) → [inst : CommRing R] → [inst_1 : LieRing L] → [inst_2 : LieAlgebra R L] → ℕ → LieIdeal R L
-- Lean.DocString.Parser
Lean.Doc.Parser.UnorderedListType.asterisk.sizeOf_spec : sizeOf Lean.Doc.Parser.UnorderedListType.asterisk = 1
-- Mathlib.Probability.Process.Stopping
MeasureTheory.stoppedValue_eq' : ∀ {Ω : Type u_1} {ι : Type u_3} [inst : Nonempty ι] {τ : Ω → WithTop ι} {E : Type u_4} {u : ι → Ω → E}
  [inst_1 : Preorder ι] [inst_2 : LocallyFiniteOrderBot ι] [inst_3 : AddCommMonoid E] {N : ι},
  (∀ (ω : Ω), τ ω ≤ ↑N) → MeasureTheory.stoppedValue u τ = ∑ i ≤ N, {ω | τ ω = ↑i}.indicator (u i)
-- Mathlib.Order.WithBot
WithBot.map₂_bot_left : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (b : WithBot β), WithBot.map₂ f ⊥ b = ⊥
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.SimplicialObject.Augmented.toArrow_obj_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject.Augmented C),
  (CategoryTheory.SimplicialObject.Augmented.toArrow.obj X).left =
    (CategoryTheory.SimplicialObject.Augmented.drop.obj X).obj (Opposite.op { len := 0 })
-- Mathlib.CategoryTheory.SingleObj
/-- Reinterpret a monoid isomorphism `f : M ≃* N` as an equivalence `SingleObj M ≌ SingleObj N`.  -/
MulEquiv.toSingleObjEquiv : {M : Type u} →
  {N : Type v} →
    [inst : Monoid M] → [inst_1 : Monoid N] → M ≃* N → (CategoryTheory.SingleObj M ≌ CategoryTheory.SingleObj N)
-- Lean.Data.Name
Lean.Name.lt : Lean.Name → Lean.Name → Bool
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getD_inter_of_not_mem_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k : α} {fallback : β k}, k ∉ t₂ → (t₁ ∩ t₂).getD k fallback = fallback
-- Lean.Data.JsonRpc
Lean.JsonRpc.MessageMetaData.toMessage : Lean.JsonRpc.MessageMetaData → Lean.JsonRpc.Message
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
Nat.reduceEqDiff : Lean.Meta.Simp.Simproc
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.isPath_iff_isSubwalk_imp_nil : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v},
  p.IsPath ↔ ∀ (v_1 : V) (w : G.Walk v_1 v_1), w.IsSubwalk p → w.Nil
-- Mathlib.Topology.Algebra.UniformConvergence
UniformFun.toFun_div : ∀ {α : Type u_1} {β : Type u_2} [inst : Div β] (f g : UniformFun α β),
  UniformFun.toFun (f / g) = UniformFun.toFun f / UniformFun.toFun g
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.nonunits_subset : ∀ {K : Type u} [inst : Field K] {A : ValuationSubring K}, ↑A.nonunits ⊆ ↑A
-- Mathlib.Analysis.BoxIntegral.Basic
BoxIntegral.HasIntegral.sub : ∀ {ι : Type u} {E : Type v} {F : Type w} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {I : BoxIntegral.Box ι} [inst_4 : Fintype ι]
  {l : BoxIntegral.IntegrationParams} {f g : (ι → ℝ) → E} {vol : BoxIntegral.BoxAdditiveMap ι (E →L[ℝ] F) ⊤} {y y' : F},
  BoxIntegral.HasIntegral I l f vol y →
    BoxIntegral.HasIntegral I l g vol y' → BoxIntegral.HasIntegral I l (f - g) vol (y - y')
-- Mathlib.Algebra.ContinuedFractions.Computation.Translations
/-- Gives a recurrence to compute the `n + 1`th value of the sequence of integer and fractional
parts of a value in case of termination.
 -/
GenContFract.IntFractPair.succ_nth_stream_eq_none_iff : ∀ {K : Type u_1} [inst : DivisionRing K] [inst_1 : LinearOrder K] [inst_2 : FloorRing K] {v : K} {n : ℕ},
  GenContFract.IntFractPair.stream v (n + 1) = none ↔
    GenContFract.IntFractPair.stream v n = none ∨ ∃ ifp, GenContFract.IntFractPair.stream v n = some ifp ∧ ifp.fr = 0
-- Std.Data.Iterators.Combinators.Monadic.Zip
Option.SomeLtNone.lt.eq_1 : ∀ {β : Type u_1} {α : Type u_2} (r : α → β → Prop) (x : Option β), Option.SomeLtNone.lt r none x = False
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.mixedEmbedding.norm_eq_sup'_normAtPlace : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] (x : NumberField.mixedEmbedding.mixedSpace K),
  ‖x‖ = Finset.univ.sup' ⋯ fun w => (NumberField.mixedEmbedding.normAtPlace w) x
-- Mathlib.Analysis.BoxIntegral.Basic
/-- If `‖f x‖ ≤ g x` on `[l, u]` and `g` is integrable, then the norm of the integral of `f` is less
than or equal to the integral of `g`.  -/
BoxIntegral.norm_integral_le_of_norm_le : ∀ {ι : Type u} {E : Type v} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {I : BoxIntegral.Box ι}
  [inst_2 : Fintype ι] {l : BoxIntegral.IntegrationParams} {f : (ι → ℝ) → E} {g : (ι → ℝ) → ℝ},
  (∀ x ∈ BoxIntegral.Box.Icc I, ‖f x‖ ≤ g x) →
    ∀ (μ : MeasureTheory.Measure (ι → ℝ)) [inst_3 : MeasureTheory.IsLocallyFiniteMeasure μ],
      BoxIntegral.Integrable I l g μ.toBoxAdditive.toSMul →
        ‖BoxIntegral.integral I l f μ.toBoxAdditive.toSMul‖ ≤ BoxIntegral.integral I l g μ.toBoxAdditive.toSMul
-- Mathlib.Data.Sym.Sym2
/-- **Alias** of the reverse direction of `Sym2.toRel_mono_iff`. -/
Sym2.toRel_mono : ∀ {α : Type u_1} (s₁ s₂ : Set (Sym2 α)), s₁ ⊆ s₂ → Sym2.ToRel s₁ ≤ Sym2.ToRel s₂
-- Init.Prelude
instDecidableEqChar : DecidableEq Char
-- Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
/-- The bijection `X.op.N ≃ X.N`.  -/
SSet.N.opEquiv : {X : SSet} → X.op.N ≃o X.N
-- Mathlib.Order.Monotone.Basic
antitone_comp_ofDual_iff : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
  Antitone (f ∘ ⇑OrderDual.ofDual) ↔ Monotone f
-- Mathlib.GroupTheory.Subgroup.Centralizer
AddSubgroup.centralizer_univ : ∀ {G : Type u_1} [inst : AddGroup G], AddSubgroup.centralizer Set.univ = AddSubgroup.center G
-- Mathlib.Geometry.Manifold.DerivationBundle
instFunLikePointedContMDiffMap : (𝕜 : Type u_1) →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_3} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {H : Type u_4} →
            [inst_3 : TopologicalSpace H] →
              (I : ModelWithCorners 𝕜 E H) →
                (M : Type u_2) →
                  [inst_4 : TopologicalSpace M] →
                    [inst_5 : ChartedSpace H M] →
                      (n : WithTop ℕ∞) → (x : M) → FunLike (PointedContMDiffMap 𝕜 I M n x) M 𝕜
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.getKey?_ofList_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} [Std.TransCmp cmp] {l : List (α × β)} {k k' : α},
  cmp k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬cmp a.1 b.1 = Ordering.eq) l →
      k ∈ List.map Prod.fst l → (Std.DTreeMap.Raw.Const.ofList l cmp).getKey? k' = some k
-- Mathlib.RingTheory.WittVector.Truncated
WittVector.liftEquiv_apply : ∀ {p : ℕ} {R : Type u_1} [inst : CommRing R] [inst_1 : Fact (Nat.Prime p)] {S : Type u_2} [inst_2 : Semiring S]
  (f : { f // ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), (TruncatedWittVector.truncate hk).comp (f k₂) = f k₁ }),
  WittVector.liftEquiv f = WittVector.lift ↑f ⋯
-- Mathlib.GroupTheory.Congruence.Defs
/-- Multiplicative congruence relations preserve natural powers.  -/
Con.pow : ∀ {M : Type u_4} [inst : Monoid M] (c : Con M) (n : ℕ) {w x : M}, c w x → c (w ^ n) (x ^ n)
-- Mathlib.GroupTheory.DivisibleHull
/-- Coercion from `M` to `DivisibleHull M` as an `AddMonoidHom`.  -/
DivisibleHull.coeAddMonoidHom : (M : Type u_1) → [inst : AddCommMonoid M] → M →+ DivisibleHull M
-- Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
exists_pow_ne_one_of_isCyclic : ∀ {G : Type u_2} [inst : Group G] [G_cyclic : IsCyclic G] {k : ℕ}, k ≠ 0 → k < Nat.card G → ∃ a, a ^ k ≠ 1
-- Init.Data.Option.Lemmas
Option.guard_true : ∀ {α : Type u_1}, (Option.guard fun x => true) = some
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomMulAct.instMulDistribMulActionForallOfMulAction : {M : Type u_1} →
  {α : Type u_3} →
    {A : Type u_5} → [inst : Monoid M] → [MulAction M α] → [inst_2 : Monoid A] → MulDistribMulAction Mᵈᵐᵃ (α → A)
-- Mathlib.CategoryTheory.Category.Preorder
CategoryTheory.homOfLE.congr_simp : ∀ {X : Type u} [inst : Preorder X] {x y : X} (h : x ≤ y), CategoryTheory.homOfLE h = CategoryTheory.homOfLE h
-- Mathlib.Algebra.Group.Submonoid.Defs
AddSubmonoid.coe_add : ∀ {M : Type u_4} [inst : AddZeroClass M] (S : AddSubmonoid M) (x y : ↥S), ↑(x + y) = ↑x + ↑y
-- Mathlib.Order.GaloisConnection.Defs
GaloisCoinsertion.strictMono_l : ∀ {α : Type u} {β : Type v} {u : α → β} {l : β → α} [inst : Preorder α] [inst_1 : Preorder β]
  (gi : GaloisCoinsertion l u), StrictMono l
-- Mathlib.Data.Int.ModEq
Int.add_modEq_right : ∀ {n a : ℤ}, a + n ≡ a [ZMOD n]
-- Std.Data.Iterators.Lemmas.Combinators.DropWhile
Std.Iter.toList_dropWhile_of_finite : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] {P : β → Bool} [Std.Iterators.Finite α Id] {it : Std.Iter β},
  (Std.Iter.dropWhile P it).toList = List.dropWhile P it.toList
-- Mathlib.Algebra.Group.Subgroup.Defs
Subgroup.Normal.conj_mem' : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G}, H.Normal → ∀ n ∈ H, ∀ (g : G), g⁻¹ * n * g ∈ H
-- Lean.Elab.Deriving.Util
Lean.Elab.Deriving.Context.auxFunNames : Lean.Elab.Deriving.Context → Array Lean.Name
-- Lean.Environment
Lean.Kernel.Environment.isDiagnosticsEnabled : Lean.Kernel.Environment → Bool
-- Mathlib.CategoryTheory.Limits.Final
CategoryTheory.Functor.Final.colimitIso_hom : ∀ {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) [inst_4 : CategoryTheory.Limits.HasColimit G],
  (CategoryTheory.Functor.Final.colimitIso F G).hom = CategoryTheory.Limits.colimit.pre G F