mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.Filter.Pointwise
Filter.eventually_smul_filter : ∀ {α : Type u_2} {β : Type u_3} [inst : SMul α β] {f : Filter β} {a : α} {p : β → Prop},
  (∀ᶠ (y : β) in a • f, p y) ↔ ∀ᶠ (x : β) in f, p (a • x)
-- Mathlib.LinearAlgebra.Prod
LinearMap.prodMap_add : ∀ {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} {M₄ : Type z} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M₃] [inst_4 : AddCommMonoid M₄] [inst_5 : Module R M]
  [inst_6 : Module R M₂] [inst_7 : Module R M₃] [inst_8 : Module R M₄] (f₁ f₂ : M →ₗ[R] M₃) (g₁ g₂ : M₂ →ₗ[R] M₄),
  (f₁ + f₂).prodMap (g₁ + g₂) = f₁.prodMap g₁ + f₂.prodMap g₂
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous
SheafOfModules.pushforwardComp_hom_app_val_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {D' : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} D'] {J : CategoryTheory.GrothendieckTopology C}
  {K : CategoryTheory.GrothendieckTopology D} {F : CategoryTheory.Functor C D} {S : CategoryTheory.Sheaf J RingCat}
  {R : CategoryTheory.Sheaf K RingCat} [inst_3 : F.IsContinuous J K]
  (φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R) {K' : CategoryTheory.GrothendieckTopology D'}
  {G : CategoryTheory.Functor D D'} {R' : CategoryTheory.Sheaf K' RingCat} [inst_4 : G.IsContinuous K K']
  (ψ : R ⟶ (G.sheafPushforwardContinuous RingCat K K').obj R') (M : SheafOfModules R') (U : Cᵒᵖ)
  (x : ↑((((SheafOfModules.pushforward ψ).comp (SheafOfModules.pushforward φ)).obj M).val.obj U)),
  (CategoryTheory.ConcreteCategory.hom (((SheafOfModules.pushforwardComp φ ψ).hom.app M).val.app U)) x = x
-- Mathlib.Logic.IsEmpty.Defs
IsEmpty.prop_iff : ∀ {p : Prop}, IsEmpty p ↔ ¬p
-- Mathlib.Condensed.Discrete.LocallyConstant
CompHausLike.LocallyConstant.functorToPresheaves_obj_obj : ∀ {P : TopCat → Prop} (X : Type (max u w)) (x : (CompHausLike P)ᵒᵖ),
  (CompHausLike.LocallyConstant.functorToPresheaves.obj X).obj x =
    match x with
    | Opposite.op S => LocallyConstant (↑S.toTop) X
-- Mathlib.LinearAlgebra.Quotient.Defs
Submodule.Quotient.eq : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (p : Submodule R M)
  {x y : M}, Submodule.Quotient.mk x = Submodule.Quotient.mk y ↔ x - y ∈ p
-- Lean.Environment
/-- Commits the signature of the constant to the main environment branch. The declaration name must
match the name originally given to `addConstAsync`. It is optional to call this function but can
help in unblocking corresponding accesses to the constant on the main branch.
 -/
Lean.Environment.AddConstAsyncResult.commitSignature : Lean.Environment.AddConstAsyncResult → Lean.ConstantVal → IO Unit
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey_alterKey : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {k k' : α} {f : Option (β k) → Option (β k)}
  (l : List ((a : α) × β a)) (hl : Std.Internal.List.DistinctKeys l)
  (hc : Std.Internal.List.containsKey k' (Std.Internal.List.alterKey k f l) = true),
  Std.Internal.List.getKey k' (Std.Internal.List.alterKey k f l) hc =
    if heq : (k == k') = true then k else Std.Internal.List.getKey k' l ⋯
-- Mathlib.Data.Sigma.Order
/-- The lexicographical preorder on a sigma type.  -/
Sigma.Lex.preorder : {ι : Type u_1} → {α : ι → Type u_2} → [Preorder ι] → [(i : ι) → Preorder (α i)] → Preorder (Σₗ (i : ι), α i)
-- Mathlib.CategoryTheory.Limits.Shapes.KernelPair
/-- If `(a,b)` is a kernel pair for `f₁ ≫ f₂` and `f₂` is mono, then `(a,b)` is a kernel pair for
just `f₁`.
The converse of `comp_of_mono`.
 -/
CategoryTheory.IsKernelPair.cancel_right_of_mono : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {R X Y Z : C} {a b : R ⟶ X} {f₁ : X ⟶ Y} {f₂ : Y ⟶ Z}
  [CategoryTheory.Mono f₂],
  CategoryTheory.IsKernelPair (CategoryTheory.CategoryStruct.comp f₁ f₂) a b → CategoryTheory.IsKernelPair f₁ a b
-- Mathlib.Algebra.Group.Opposite
AddOpposite.instSubtractionCommMonoid : {α : Type u_1} → [SubtractionCommMonoid α] → SubtractionCommMonoid αᵃᵒᵖ
-- Mathlib.Data.PFunctor.Multivariate.W
MvPFunctor.comp_wPathCasesOn : ∀ {n : ℕ} (P : MvPFunctor.{u} (n + 1)) {α : TypeVec.{u_1} n} {β : TypeVec.{u_2} n} (h : α.Arrow β) {a : P.A}
  {f : P.last.B a → P.last.W} (g' : (P.drop.B a).Arrow α) (g : (j : P.last.B a) → TypeVec.Arrow (P.WPath (f j)) α),
  TypeVec.comp h (P.wPathCasesOn g' g) = P.wPathCasesOn (TypeVec.comp h g') fun i => TypeVec.comp h (g i)
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.eq_C_of_degree_eq_zero : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p.degree = 0 → p = Polynomial.C (p.coeff 0)
-- Init.Data.Array.Lemmas
Array.mapM_eq_foldlM : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] [LawfulMonad m] {f : α → m β} {xs : Array α},
  Array.mapM f xs = Array.foldlM (fun bs a => bs.push <$> f a) #[] xs
-- Mathlib.Algebra.GroupWithZero.Basic
IsNilpotent.zero : ∀ {R : Type u_3} [inst : MonoidWithZero R], IsNilpotent 0
-- Mathlib.Data.Fin.Tuple.Basic
Fin.modNat.eq_1 : ∀ {m n : ℕ} (i : Fin (m * n)), i.modNat = ⟨↑i % n, ⋯⟩
-- Mathlib.GroupTheory.PresentedGroup
PresentedGroup.one_of_mem : ∀ {α : Type u_1} {rels : Set (FreeGroup α)} {x : FreeGroup α}, x ∈ rels → (PresentedGroup.mk rels) x = 1
-- Mathlib.Algebra.Lie.DirectSum
DirectSum.lieAlgebra_ext : ∀ (R : Type u) (ι : Type v) [inst : CommRing R] (L : ι → Type w) [inst_1 : (i : ι) → LieRing (L i)]
  [inst_2 : (i : ι) → LieAlgebra R (L i)] {x y : DirectSum ι fun i => L i},
  (∀ (i : ι), (DirectSum.lieAlgebraComponent R ι L i) x = (DirectSum.lieAlgebraComponent R ι L i) y) → x = y
-- Mathlib.Dynamics.BirkhoffSum.Average
birkhoffAverage_add : ∀ (R : Type u_1) {α : Type u_2} {M : Type u_3} [inst : DivisionSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] {f : α → α} {g g' : α → M},
  birkhoffAverage R f (g + g') = birkhoffAverage R f g + birkhoffAverage R f g'
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.mem_neg : ∀ {α : Type u_2} [inst : Neg α] {s : Set α} {a : α}, a ∈ -s ↔ -a ∈ s
-- Mathlib.Algebra.Star.StarAlgHom
NonUnitalStarAlgHom.comp_assoc : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} {D : Type u_5} [inst : Monoid R]
  [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : DistribMulAction R A] [inst_3 : Star A]
  [inst_4 : NonUnitalNonAssocSemiring B] [inst_5 : DistribMulAction R B] [inst_6 : Star B]
  [inst_7 : NonUnitalNonAssocSemiring C] [inst_8 : DistribMulAction R C] [inst_9 : Star C]
  [inst_10 : NonUnitalNonAssocSemiring D] [inst_11 : DistribMulAction R D] [inst_12 : Star D] (f : C →⋆ₙₐ[R] D)
  (g : B →⋆ₙₐ[R] C) (h : A →⋆ₙₐ[R] B), (f.comp g).comp h = f.comp (g.comp h)
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
mul_nonpos_iff_pos_imp_nonpos : ∀ {R : Type u} [inst : Ring R] [inst_1 : LinearOrder R] {a b : R} [PosMulStrictMono R] [MulPosStrictMono R]
  [AddLeftMono R] [AddLeftReflectLE R], a * b ≤ 0 ↔ (0 < a → b ≤ 0) ∧ (b < 0 → 0 ≤ a)
-- Mathlib.Analysis.LocallyConvex.WithSeminorms
SeminormFamily.basisSets_iff : ∀ {R : Type u_1} {E : Type u_6} {ι : Type u_9} [inst : SeminormedRing R] [inst_1 : AddCommGroup E] [inst_2 : Module R E]
  (p : SeminormFamily R E ι) {U : Set E}, U ∈ p.basisSets ↔ ∃ i r, 0 < r ∧ U = (i.sup p).ball 0 r
-- Mathlib.Data.Setoid.Partition
Setoid.card_classes_ker_le : ∀ {α : Type u_2} {β : Type u_3} [inst : Fintype β] (f : α → β) [inst_1 : Fintype ↑(Setoid.ker f).classes],
  Fintype.card ↑(Setoid.ker f).classes ≤ Fintype.card β
-- Mathlib.GroupTheory.Schreier
card_dvd_exponent_pow_rank : ∀ (G : Type u_1) [inst : CommGroup G] [inst_1 : Group.FG G], Nat.card G ∣ Monoid.exponent G ^ Group.rank G
-- Mathlib.Analysis.InnerProductSpace.Harmonic.Basic
/-- Compositions of continuous `ℝ`-linear maps with harmonic functions are harmonic.
 -/
InnerProductSpace.HarmonicAt.comp_CLM : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  {F : Type u_2} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] {G : Type u_3}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace ℝ G] {f : E → F} {x : E},
  InnerProductSpace.HarmonicAt f x → ∀ (l : F →L[ℝ] G), InnerProductSpace.HarmonicAt (⇑l ∘ f) x
-- Mathlib.Probability.Kernel.Composition.Prod
ProbabilityTheory.Kernel.IsSFiniteKernel.prod : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) (η : ProbabilityTheory.Kernel α γ),
  ProbabilityTheory.IsSFiniteKernel (κ.prod η)
-- Mathlib.Analysis.InnerProductSpace.Orthonormal
Orthonormal.equiv_toLinearEquiv : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_4} {ι' : Type u_5} {E' : Type u_7} [inst_3 : SeminormedAddCommGroup E'] [inst_4 : InnerProductSpace 𝕜 E']
  {v : Module.Basis ι 𝕜 E} (hv : Orthonormal 𝕜 ⇑v) {v' : Module.Basis ι' 𝕜 E'} (hv' : Orthonormal 𝕜 ⇑v') (e : ι ≃ ι'),
  (hv.equiv hv' e).toLinearEquiv = v.equiv v' e
-- Mathlib.Order.Filter.IsBounded
Filter.IsBoundedUnder.isCoboundedUnder_flip : ∀ {α : Type u_1} {γ : Type u_3} {r : α → α → Prop} {u : γ → α} {l : Filter γ} [IsTrans α r] [l.NeBot],
  Filter.IsBoundedUnder r l u → Filter.IsCoboundedUnder (flip r) l u
-- Mathlib.Combinatorics.Quiver.Covering
/-- A prefunctor induces a map of `Quiver.Costar` at every vertex.  -/
Prefunctor.costar : {U : Type u_1} →
  [inst : Quiver U] →
    {V : Type u_2} → [inst_1 : Quiver V] → (φ : U ⥤q V) → (u : U) → Quiver.Costar u → Quiver.Costar (φ.obj u)
-- Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Asymptotics.IsEquivalent.trans_isTheta : ∀ {α : Type u_1} {β : Type u_2} {β₂ : Type u_3} [inst : NormedAddCommGroup β] [inst_1 : Norm β₂] {l : Filter α}
  {f g₁ : α → β} {g₂ : α → β₂}, Asymptotics.IsEquivalent l f g₁ → g₁ =Θ[l] g₂ → f =Θ[l] g₂
-- Mathlib.Tactic.TermCongr
Mathlib.Tactic.TermCongr.CongrResult.mk.injEq : ∀ (lhs rhs : Lean.Expr) (pf? : Option (Mathlib.Tactic.TermCongr.CongrType → Lean.MetaM Lean.Expr))
  (lhs_1 rhs_1 : Lean.Expr) (pf?_1 : Option (Mathlib.Tactic.TermCongr.CongrType → Lean.MetaM Lean.Expr)),
  ({ lhs := lhs, rhs := rhs, pf? := pf? } = { lhs := lhs_1, rhs := rhs_1, pf? := pf?_1 }) =
    (lhs = lhs_1 ∧ rhs = rhs_1 ∧ pf? = pf?_1)
-- Mathlib.CategoryTheory.Sites.Over
CategoryTheory.Sieve.overEquiv_preOneHypercover_sieve₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} {Y : CategoryTheory.Over X}
  (E : CategoryTheory.PreOneHypercover Y) {i₁ i₂ : E.I₀} {W : CategoryTheory.Over X} (p₁ : W ⟶ E.X i₁)
  (p₂ : W ⟶ E.X i₂),
  (CategoryTheory.Sieve.overEquiv W) (E.sieve₁ p₁ p₂) =
    (E.map (CategoryTheory.Over.forget X)).sieve₁ (CategoryTheory.Over.Hom.left p₁) (CategoryTheory.Over.Hom.left p₂)
-- Mathlib.Analysis.Meromorphic.Basic
MeromorphicOn.sub : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f g : 𝕜 → E} {U : Set 𝕜}, MeromorphicOn f U → MeromorphicOn g U → MeromorphicOn (f - g) U
-- Mathlib.Combinatorics.Additive.ETransform
Finset.addETransformRight.card : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : AddGroup α] (e : α) (x : Finset α × Finset α),
  (Finset.addETransformLeft e x).2.card + (Finset.addETransformRight e x).2.card = 2 * x.2.card
-- Mathlib.Order.Interval.Set.Basic
Set.Ioi_True : Set.Ioi True = ∅
-- Mathlib.Analysis.CStarAlgebra.Classes
MulOpposite.instNonUnitalCStarAlgebra : {A : Type u_1} → [NonUnitalCStarAlgebra A] → NonUnitalCStarAlgebra Aᵐᵒᵖ
-- Mathlib.CategoryTheory.Simple
CategoryTheory.Simple.mono_isIso_iff_nonzero : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.Limits.HasZeroMorphisms C} {X : C}
  [self : CategoryTheory.Simple X] {Y : C} (f : Y ⟶ X) [CategoryTheory.Mono f], CategoryTheory.IsIso f ↔ f ≠ 0
-- Mathlib.Topology.Category.UniformSpace
/-- A (bundled) complete separated uniform space.  -/
CpltSepUniformSpace : Type (u + 1)
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.add_linear : ∀ {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} [inst : Ring k] [inst_1 : AddCommGroup V1]
  [inst_2 : Module k V1] [inst_3 : AddTorsor V1 P1] [inst_4 : AddCommGroup V2] [inst_5 : Module k V2]
  (f g : P1 →ᵃ[k] V2), (f + g).linear = f.linear + g.linear
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.Ring.type : Lean.Meta.Grind.Arith.CommRing.Ring → Lean.Expr
-- Mathlib.Dynamics.PeriodicPts.Defs
Function.periodicOrbit_apply_iterate_eq : ∀ {α : Type u_1} {f : α → α} {x : α},
  x ∈ Function.periodicPts f → ∀ (n : ℕ), Function.periodicOrbit f (f^[n] x) = Function.periodicOrbit f x
-- Mathlib.Condensed.Discrete.Module
/-- The functor from the category of `R`-modules to presheaves on `CompHausLike P` given by locally
constant maps.
 -/
CompHausLike.LocallyConstantModule.functorToPresheaves : {P : TopCat → Prop} →
  (R : Type (max u w)) →
    [inst : Ring R] → CategoryTheory.Functor (ModuleCat R) (CategoryTheory.Functor (CompHausLike P)ᵒᵖ (ModuleCat R))
-- Mathlib.CategoryTheory.Limits.IsConnected
/-- The functor mapping every object to `PUnit`.  -/
CategoryTheory.Limits.Types.constPUnitFunctor : (C : Type u) → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.Functor C (Type w)
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.dvd_comp_X_sub_C_iff : ∀ {R : Type u} [inst : CommRing R] (p q : Polynomial R) (a : R),
  p ∣ q.comp (Polynomial.X - Polynomial.C a) ↔ p.comp (Polynomial.X + Polynomial.C a) ∣ q
-- Mathlib.CategoryTheory.Monoidal.Subcategory
CategoryTheory.ObjectProperty.TensorLE.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {P₁ P₂ Q : CategoryTheory.ObjectProperty C},
  (∀ (X₁ X₂ : C), P₁ X₁ → P₂ X₂ → Q (CategoryTheory.MonoidalCategoryStruct.tensorObj X₁ X₂)) → P₁.TensorLE P₂ Q
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.Cont'.brecOn.go : {motive : Turing.PartrecToTM2.Cont' → Sort u} →
  (t : Turing.PartrecToTM2.Cont') →
    ((t : Turing.PartrecToTM2.Cont') → Turing.PartrecToTM2.Cont'.below t → motive t) →
      motive t ×' Turing.PartrecToTM2.Cont'.below t
-- Mathlib.MeasureTheory.Function.LpSpace.Indicator
MeasureTheory.nnnorm_indicatorConstLp_le : ∀ {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] {s : Set α} {hs : MeasurableSet s} {hμs : μ s ≠ ⊤} {c : E},
  ‖MeasureTheory.indicatorConstLp p hs hμs c‖₊ ≤ ‖c‖₊ * (μ s).toNNReal ^ (1 / p.toReal)
-- Init.Data.List.MinMax
_private.Init.Data.List.MinMax.0.List.getLast?.match_1.splitter : {α : Type u_1} →
  (motive : List α → Sort u_2) →
    (x : List α) → (Unit → motive []) → ((a : α) → (as : List α) → motive (a :: as)) → motive x
-- Mathlib.Analysis.Normed.MulAction
NormMulClass.toNormSMulClass : ∀ {α : Type u_1} [inst : Norm α] [inst_1 : Mul α] [NormMulClass α], NormSMulClass α α
-- Mathlib.Analysis.SpecificLimits.Normed
/-- If `0 ≤ r < 1`, then `n * r ^ n` tends to zero. This is a specialized version of
`tendsto_self_mul_const_pow_of_abs_lt_one`, singled out for ease of application.  -/
tendsto_self_mul_const_pow_of_lt_one : ∀ {r : ℝ}, 0 ≤ r → r < 1 → Filter.Tendsto (fun n => ↑n * r ^ n) Filter.atTop (nhds 0)
-- Mathlib.Analysis.InnerProductSpace.Orthonormal
Orthonormal.equiv_apply : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_4} {E' : Type u_7} [inst_3 : SeminormedAddCommGroup E'] [inst_4 : InnerProductSpace 𝕜 E'] {ι' : Type u_9}
  {v : Module.Basis ι 𝕜 E} (hv : Orthonormal 𝕜 ⇑v) {v' : Module.Basis ι' 𝕜 E'} (hv' : Orthonormal 𝕜 ⇑v') (e : ι ≃ ι')
  (i : ι), (hv.equiv hv' e) (v i) = v' (e i)
-- Mathlib.Topology.Instances.EReal.Lemmas
EReal.limsup_add_le_of_le : ∀ {α : Type u_3} {f : Filter α} {u v : α → EReal} {a b : EReal},
  Filter.limsup u f < a → Filter.limsup v f ≤ b → Filter.limsup (u + v) f ≤ a + b
-- Mathlib.Topology.Algebra.Monoid
AddSubmonoid.mem_nhds_zero : ∀ {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : AddCommMonoid M] (S : AddSubmonoid M), IsOpen ↑S → ↑S ∈ nhds 0
-- Mathlib.Algebra.Group.Action.Prod
smulMulHom_apply : ∀ {α : Type u_5} {β : Type u_6} [inst : Monoid α] [inst_1 : Mul β] [inst_2 : MulAction α β]
  [inst_3 : IsScalarTower α β β] [inst_4 : SMulCommClass α β β] (a : α × β), smulMulHom a = a.1 • a.2
-- Mathlib.Order.SuccPred.Limit
Order.IsSuccLimit.isMax : ∀ {α : Type u_1} {a : α} [inst : Preorder α] [inst_1 : SuccOrder α], Order.IsSuccLimit (Order.succ a) → IsMax a
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.forIn_iterM_id : ∀ {α β γ : Type u} {m : Type u → Type w} {Pred EPred : Type u} [inst : Monad m]
  [inst_1 : Std.Internal.Do.Assertion Pred] [inst_2 : Std.Internal.Do.Assertion EPred]
  [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] [inst_4 : Std.Iterator α Id β] [Std.Iterators.Finite α Id]
  [inst_6 : Std.IteratorLoop α Id m] [Std.LawfulIteratorLoop α Id m] {init : γ} {f : β → γ → m (ForInStep γ)}
  {it : Std.IterM Id β} (inv : Std.Internal.Do.Invariant it.toList.run γ Pred) {epost : EPred},
  (∀ (pref : List β) (cur : β) (suff : List β) (h : it.toList.run = pref ++ cur :: suff) (b : γ),
      ⦃ inv { «prefix» := pref, suffix := cur :: suff, property := ⋯ } b ⦄ f cur b ⦃ fun r =>
        match r with
        | ForInStep.yield b' => inv { «prefix» := pref ++ [cur], suffix := suff, property := ⋯ } b'
        | ForInStep.done b' => inv { «prefix» := it.toList.run, suffix := [], property := ⋯ } b';
        epost ⦄) →
    ⦃ inv { «prefix» := [], suffix := it.toList.run, property := ⋯ } init ⦄ forIn it init f ⦃ fun b =>
      inv { «prefix» := it.toList.run, suffix := [], property := ⋯ } b; epost ⦄
-- Mathlib.Topology.Order.LeftRight
nhdsLT_sup_nhdsGE : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] (a : α),
  nhdsWithin a (Set.Iio a) ⊔ nhdsWithin a (Set.Ici a) = nhds a
-- Mathlib.Topology.Bornology.Hom
LocallyBoundedMapClass.mk : ∀ {F : Type u_6} {α : outParam (Type u_7)} {β : outParam (Type u_8)} [inst : Bornology α] [inst_1 : Bornology β]
  [inst_2 : FunLike F α β],
  (∀ (f : F), Filter.comap (⇑f) (Bornology.cobounded β) ≤ Bornology.cobounded α) → LocallyBoundedMapClass F α β
-- Mathlib.Geometry.RingedSpace.OpenImmersion
/-- A variant of `app_inv_app` that gives an `eqToHom` instead of `homOfLe`.  -/
AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.app_inv_app' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : AlgebraicGeometry.PresheafedSpace C} (f : X ⟶ Y)
  [H : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f] (U : TopologicalSpace.Opens ↑↑Y)
  (hU : ↑U ⊆ Set.range ⇑(CategoryTheory.ConcreteCategory.hom f.base)),
  CategoryTheory.CategoryStruct.comp (f.c.app (Opposite.op U))
      (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp f ((TopologicalSpace.Opens.map f.base).obj U)) =
    Y.presheaf.map (CategoryTheory.eqToHom ⋯).op
-- Mathlib.Topology.MetricSpace.Isometry
/-- **Alias** of `IsometryEquiv.preimage_closedEBall`. -/
IsometryEquiv.preimage_emetric_closedBall : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] (h : α ≃ᵢ β) (x : β)
  (r : ENNReal), ⇑h ⁻¹' Metric.closedEBall x r = Metric.closedEBall (h.symm x) r
-- Mathlib.CategoryTheory.Dialectica.Monoidal
CategoryTheory.Dial.rightUnitorImpl_hom_F : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasFiniteProducts C]
  [inst_2 : CategoryTheory.Limits.HasPullbacks C] (X : CategoryTheory.Dial C),
  X.rightUnitorImpl.hom.F =
    CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.snd
      (CategoryTheory.Limits.terminal.from ((X.src ⨯ ⊤_ C) ⨯ X.tgt))
-- Mathlib.CategoryTheory.Equivalence
/-- Compatibility of `changeFunctor` with identity isomorphisms of functors  -/
CategoryTheory.Equivalence.changeFunctor_refl : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : C ≌ D), e.changeFunctor (CategoryTheory.Iso.refl e.functor) = e
-- Mathlib.Analysis.Analytic.CPolynomialDef
HasFiniteFPowerSeriesOnBall.congr : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f g : E → F}
  {p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal} {n : ℕ},
  HasFiniteFPowerSeriesOnBall f p x n r → Set.EqOn f g (Metric.eball x r) → HasFiniteFPowerSeriesOnBall g p x n r
-- Init.Data.Rat.Lemmas
Rat.lt_floor : ∀ {x : ℚ}, x - 1 < ↑x.floor
-- Mathlib.GroupTheory.Commensurable
Subgroup.Commensurable.comm : ∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G}, H.Commensurable K ↔ K.Commensurable H
-- Mathlib.Algebra.Order.ToIntervalMod
toIcoDiv_add_intCast_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 : ℤ), toIcoDiv hp (a + ↑m * p) b = toIcoDiv hp a b - m
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.instIsIsoMapOfEpi : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  (f : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasCokernel f] {X' Y' : C} (f' : X' ⟶ Y')
  [inst_3 : CategoryTheory.Limits.HasCokernel f'] (p : X ⟶ X') (q : Y ⟶ Y')
  (w : CategoryTheory.CategoryStruct.comp f q = CategoryTheory.CategoryStruct.comp p f') [CategoryTheory.Epi p]
  [CategoryTheory.IsIso q], CategoryTheory.IsIso (CategoryTheory.Limits.cokernel.map f f' p q w)
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
Std.DHashMap.Internal.AssocList.toList_erase : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {l : Std.DHashMap.Internal.AssocList α β} {a : α},
  (Std.DHashMap.Internal.AssocList.erase a l).toList = Std.Internal.List.eraseKey a l.toList
-- Mathlib.MeasureTheory.Integral.Bochner.L1
MeasureTheory.L1.SimpleFunc.integral_congr : ∀ {α : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_1 : NormedSpace ℝ E] {f g : ↥(α →₁ₛ[μ] E)},
  ⇑(MeasureTheory.Lp.simpleFunc.toSimpleFunc f) =ᵐ[μ] ⇑(MeasureTheory.Lp.simpleFunc.toSimpleFunc g) →
    MeasureTheory.L1.SimpleFunc.integral f = MeasureTheory.L1.SimpleFunc.integral g
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
PeriodPair.weierstrassPExcept_add : ∀ (L : PeriodPair) (l₀ : ↥L.lattice) (z : ℂ),
  L.weierstrassPExcept (↑l₀) z + (1 / (z - ↑l₀) ^ 2 - 1 / ↑l₀ ^ 2) = L.weierstrassP z
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.whiskerLeft_id : ∀ {B : Type u} [self : CategoryTheory.Bicategory B] {a b c : B} (f : a ⟶ b) (g : b ⟶ c),
  CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.CategoryStruct.id g) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.comp f g)
-- Mathlib.AlgebraicTopology.ModelCategory.FundamentalLemma
HomotopicalAlgebra.RightHomotopyRel.iff_map_eq : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.ModelCategory C]
  {H : Type u_2} [inst_2 : CategoryTheory.Category.{v_2, u_2} H] (L : CategoryTheory.Functor C H)
  [L.IsLocalization (HomotopicalAlgebra.weakEquivalences C)] (X Y : C) [HomotopicalAlgebra.IsCofibrant X]
  [HomotopicalAlgebra.IsFibrant Y] {f g : X ⟶ Y}, HomotopicalAlgebra.RightHomotopyRel f g ↔ L.map f = L.map g
-- Mathlib.Algebra.Category.ModuleCat.Semi
SemimoduleCat.homLinearEquiv_symm_apply : ∀ {R : Type u} [inst : Semiring R] {M N : SemimoduleCat R} {S : Type u_1} [inst_1 : Semiring S] [inst_2 : Module S ↑N]
  [inst_3 : SMulCommClass R S ↑N] (a : ↑M →ₗ[R] ↑N),
  SemimoduleCat.homLinearEquiv.symm a = SemimoduleCat.homAddEquiv.invFun a
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.insert_eq_insert : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} {p : (a : α) × β a},
  insert p t = t.insert p.fst p.snd