mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.maxKey!_insertIfNew : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [inst : Inhabited α]
  {k : α} {v : β}, (t.insertIfNew k v).maxKey! = t.maxKey?.elim k fun k' => if cmp k' k = Ordering.lt then k else k'
-- Mathlib.GroupTheory.FreeGroup.IsFreeGroup
FreeGroupBasis.lift_symm_apply : ∀ {ι : Type u_1} {G : Type u_3} {H : Type u_4} [inst : Group G] [inst_1 : Group H] (b : FreeGroupBasis ι G) (a : G →* H)
  (a_1 : ι), b.lift.symm a a_1 = a (b.repr.symm (FreeGroup.of a_1))
-- Lean.PrettyPrinter.Delaborator.Options
Lean.getPPMVarsLevels : Lean.Options → Bool
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal
/-- If `G` preserves initial objects, then the initial comparison map for `G` is an isomorphism.  -/
CategoryTheory.Limits.PreservesInitial.iso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (G : CategoryTheory.Functor C D) →
          [inst_2 : CategoryTheory.Limits.HasInitial C] →
            [inst_3 : CategoryTheory.Limits.HasInitial D] →
              [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) G] → G.obj (⊥_ C) ≅ ⊥_ D
-- Mathlib.Topology.Algebra.Module.Spaces.WeakBilin
/-- The coercion `(fun x y => B x y) : E → (F → 𝕜)` is an embedding.  -/
WeakBilin.isEmbedding : ∀ {𝕜 : Type u_2} {E : Type u_4} {F : Type u_5} [inst : TopologicalSpace 𝕜] [inst_1 : CommSemiring 𝕜]
  [inst_2 : AddCommMonoid E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommMonoid F] [inst_5 : Module 𝕜 F]
  {B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜}, Function.Injective ⇑B → Topology.IsEmbedding fun x y => (B x) y
-- Mathlib.Combinatorics.Young.YoungDiagram
YoungDiagram.transpose_le_iff : ∀ {μ ν : YoungDiagram}, μ.transpose ≤ ν.transpose ↔ μ ≤ ν
-- Mathlib.Topology.Convenient.Category
ContinuousGeneratedByCat.of.inj : ∀ {ι : Type t} {X : ι → Type u} {inst : (i : ι) → TopologicalSpace (X i)} {carrier : Type v}
  {str : TopologicalSpace carrier} {carrier_1 : Type v} {str_1 : TopologicalSpace carrier_1},
  { carrier := carrier, str := str } = { carrier := carrier_1, str := str_1 } → carrier = carrier_1 ∧ str ≍ str_1
-- Init.Data.String.Lemmas.Pattern.Pred
String.Slice.Pattern.Model.CharPred.Decidable.isLongestRevMatchAt_of_get : ∀ {p : Char → Prop} [inst : DecidablePred p] {s : String.Slice} {pos : s.Pos} {h : pos ≠ s.startPos},
  p ((pos.prev h).get ⋯) → String.Slice.Pattern.Model.IsLongestRevMatchAt p (pos.prev h) pos
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.eq_empty_iff_size_eq_zero : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [Std.TransCmp cmp], t = ∅ ↔ t.size = 0
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
summable_nat_add_iff : ∀ {G : Type u_2} [inst : AddCommGroup G] [inst_1 : TopologicalSpace G] [IsTopologicalAddGroup G] {f : ℕ → G} (k : ℕ),
  (Summable fun n => f (n + k)) ↔ Summable f
-- Mathlib.Order.WithBot
WithTop.semilatticeInf : {α : Type u_1} → [SemilatticeInf α] → SemilatticeInf (WithTop α)
-- Mathlib.Algebra.Polynomial.Splits
Polynomial.Splits.natDegree_eq_one_of_irreducible : ∀ {R : Type u_1} [inst : Field R] {f : Polynomial R}, f.Splits → Irreducible f → f.natDegree = 1
-- Init.Prelude
/-- `if c then t else e` is notation for `ite c t e`, "if-then-else", which decides to
return `t` or `e` depending on whether `c` is true or false. The explicit argument
`c : Prop` does not have any actual computational content, but there is an additional
`[Decidable c]` argument synthesized by typeclass inference which actually
determines how to evaluate `c` to true or false. Write `if h : c then t else e`
instead for a "dependent if-then-else" `dite`, which allows `t`/`e` to use the fact
that `c` is true/false.
 -/
ite : {α : Sort u} → (c : Prop) → [h : Decidable c] → α → α → α
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.prod_range_succ : ∀ {M : Type u_4} [inst : CommMonoid M] (f : ℕ → M) (n : ℕ),
  ∏ x ∈ Finset.range (n + 1), f x = (∏ x ∈ Finset.range n, f x) * f n
-- Mathlib.Order.Filter.Extr
IsMaxFilter.max : ∀ {α : Type u} {β : Type v} [inst : LinearOrder β] {f g : α → β} {a : α} {l : Filter α},
  IsMaxFilter f l a → IsMaxFilter g l a → IsMaxFilter (fun x => max (f x) (g x)) l a
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
/-- Paste two pullback squares "vertically" to obtain another pullback square.

The objects in the statement fit into the following diagram:
```
X₁₁ - h₁₁ -> X₁₂
|            |
v₁₁          v₁₂
↓            ↓
X₂₁ - h₂₁ -> X₂₂
|            |
v₂₁          v₂₂
↓            ↓
X₃₁ - h₃₁ -> X₃₂
```
 -/
CategoryTheory.IsPullback.paste_vert : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X₁₁ X₁₂ X₂₁ X₂₂ X₃₁ X₃₂ : C} {h₁₁ : X₁₁ ⟶ X₁₂}
  {h₂₁ : X₂₁ ⟶ X₂₂} {h₃₁ : X₃₁ ⟶ X₃₂} {v₁₁ : X₁₁ ⟶ X₂₁} {v₁₂ : X₁₂ ⟶ X₂₂} {v₂₁ : X₂₁ ⟶ X₃₁} {v₂₂ : X₂₂ ⟶ X₃₂},
  CategoryTheory.IsPullback h₁₁ v₁₁ v₁₂ h₂₁ →
    CategoryTheory.IsPullback h₂₁ v₂₁ v₂₂ h₃₁ →
      CategoryTheory.IsPullback h₁₁ (CategoryTheory.CategoryStruct.comp v₁₁ v₂₁)
        (CategoryTheory.CategoryStruct.comp v₁₂ v₂₂) h₃₁
-- Mathlib.Algebra.Ring.Shrink
Shrink.instNonUnitalSemiring : {α : Type u_1} → [inst : Small.{v, u_1} α] → [NonUnitalSemiring α] → NonUnitalSemiring (Shrink.{v, u_1} α)
-- Std.Http.Server.Connection
_private.Std.Http.Server.Connection.0.Std.Http.Server.Connection.Recv.bytes.injEq : ∀ {β : Type} (x x_1 : Option ByteArray),
  (Std.Http.Server.Connection.Recv.bytes✝ x = Std.Http.Server.Connection.Recv.bytes✝ x_1) = (x = x_1)
-- Mathlib.Algebra.Group.Basic
pow_dite : ∀ {α : Type u_1} {β : Type u_2} [inst : Pow α β] (p : Prop) [inst_1 : Decidable p] (a : α) (b : p → β) (c : ¬p → β),
  (a ^ if h : p then b h else c h) = if h : p then a ^ b h else a ^ c h
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr.0.Std.Tactic.BVDecide.BVExpr.bitblast.goCache.match_1.eq_1 : ∀ {w : ℕ} (aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit) (motive : Std.Tactic.BVDecide.BVExpr.Return aig w → Sort u_1)
  (result : aig.ExtendingRefVecEntry w) (cache : Std.Tactic.BVDecide.BVExpr.Cache (↑result).aig)
  (h_1 :
    (result : aig.ExtendingRefVecEntry w) →
      (cache : Std.Tactic.BVDecide.BVExpr.Cache (↑result).aig) → motive { result := result, cache := cache }),
  (match { result := result, cache := cache } with
    | { result := result, cache := cache } => h_1 result cache) =
    h_1 result cache
-- Mathlib.Geometry.Manifold.IsManifold.Basic
ModelWithCorners.symm_comp_self : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] (I : ModelWithCorners 𝕜 E H),
  ↑I.symm ∘ ↑I = id
-- Mathlib.CategoryTheory.Idempotents.HomologicalComplex
CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_functor_obj_d_f : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] (α : Type u_3)
  [inst_2 : AddRightCancelSemigroup α] [inst_3 : One α]
  (P : CategoryTheory.Idempotents.Karoubi (HomologicalComplex C (ComplexShape.up α))) (i j : α),
  (((CategoryTheory.Idempotents.karoubiCochainComplexEquivalence C α).functor.obj P).d i j).f =
    CategoryTheory.CategoryStruct.comp (P.X.d i j) (P.p.f j)
-- Mathlib.GroupTheory.OreLocalization.Basic
OreLocalization.universalMulHom_apply : ∀ {R : Type u_1} [inst : Monoid R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S] {T : Type u_2}
  [inst_2 : Monoid T] (f : R →* T) (fS : ↥S →* Tˣ) (hf : ∀ (s : ↥S), f ↑s = ↑(fS s)) {r : R} {s : ↥S},
  (OreLocalization.universalMulHom f fS hf) (r /ₒ s) = ↑(fS s)⁻¹ * f r
-- Mathlib.Data.Set.Semiring
SetSemiring.instNonUnitalNonAssocSemiring : {α : Type u_1} → [Mul α] → NonUnitalNonAssocSemiring (SetSemiring α)
-- Mathlib.Analysis.Calculus.FDeriv.Mul
/-- At an invertible element `x` of a normed division algebra `R`, the Fréchet derivative of the
inversion operation is the linear map `fun t ↦ - x⁻¹ * t * x⁻¹`. For a nicer formula in the
commutative case, see `hasFDerivAt_inv`.  -/
hasFDerivAt_inv' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {R : Type u_5} [inst_1 : NormedDivisionRing R]
  [inst_2 : NormedAlgebra 𝕜 R] {x : R},
  x ≠ 0 → HasFDerivAt Inv.inv (-((ContinuousLinearMap.mulLeftRight 𝕜 R) x⁻¹) x⁻¹) x
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Int
_private.Lean.Meta.Tactic.Simp.BuiltinSimprocs.Int.0.Int.reduceBin : Lean.Name → ℕ → (ℤ → ℤ → ℤ) → Lean.Expr → Lean.Meta.SimpM Lean.Meta.Simp.DStep
-- Lean.Meta.Match.MatcherInfo
/-- Number of parameters  -/
Lean.Meta.Match.MatcherInfo.numParams : Lean.Meta.MatcherInfo → ℕ
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
/-- The map `S → X →ₗ[R] Y` given by `fun s x => s • (g x)`
 -/
ModuleCat.ExtendRestrictScalarsAdj.HomEquiv.evalAt : {R : Type u₁} →
  {S : Type u₂} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        (f : R →+* S) →
          {X : ModuleCat R} →
            {Y : ModuleCat S} →
              S →
                (X ⟶ (ModuleCat.restrictScalars f).obj Y) →
                  have this := Module.compHom (↑Y) f;
                  ↑X →ₗ[R] ↑Y
-- Mathlib.RingTheory.Localization.Module
/-- The `S⁻¹R`-linear maps between two `S⁻¹R`-modules are exactly the `R`-linear maps.  -/
LinearMap.extendScalarsOfIsLocalizationEquiv : {R : Type u_3} →
  [inst : CommSemiring R] →
    (S : Submonoid R) →
      (A : Type u_4) →
        [inst_1 : CommSemiring A] →
          [inst_2 : Algebra R A] →
            [IsLocalization S A] →
              {M : Type u_5} →
                {N : Type u_6} →
                  [inst_4 : AddCommMonoid M] →
                    [inst_5 : Module R M] →
                      [inst_6 : Module A M] →
                        [IsScalarTower R A M] →
                          [inst_8 : AddCommMonoid N] →
                            [inst_9 : Module R N] →
                              [inst_10 : Module A N] → [inst_11 : IsScalarTower R A N] → (M →ₗ[R] N) ≃ₗ[A] M →ₗ[A] N
-- Mathlib.Order.RelClasses
LE.total : ∀ {α : Type u} [inst : LinearOrder α], Std.Total fun x1 x2 => x1 ≤ x2
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
AlgebraicGeometry.instQuasiSeparatedToSpecΓOfQuasiSeparatedSpaceCarrierCarrierCommRingCat : ∀ {X : AlgebraicGeometry.Scheme} [QuasiSeparatedSpace ↥X], AlgebraicGeometry.QuasiSeparated X.toSpecΓ
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology
/-- The homology of `HomComplex K L` in degree `n` identifies to `CohomologyClass K L n`.  -/
CochainComplex.HomComplex.homologyAddEquiv : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      (K L : CochainComplex C ℤ) →
        (n : ℤ) → ↑(HomologicalComplex.homology (K.HomComplex L) n) ≃+ CochainComplex.HomComplex.CohomologyClass K L n
-- Mathlib.GroupTheory.Commutator.Basic
AddSubgroup.addCommutator_normal : ∀ {G : Type u_1} [inst : AddGroup G] (H₁ H₂ : AddSubgroup G) [h₁ : H₁.Normal] [h₂ : H₂.Normal], ⁅H₁, H₂⁆.Normal
-- Mathlib.Topology.Order.LocalExtr
IsLocalMaxOn.sub : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : AddCommGroup β] [inst_2 : PartialOrder β]
  [IsOrderedAddMonoid β] {f g : α → β} {a : α} {s : Set α},
  IsLocalMaxOn f s a → IsLocalMinOn g s a → IsLocalMaxOn (fun x => f x - g x) s a
-- Mathlib.GroupTheory.GroupAction.FixedPoints
/-- In a multiplicative group action, the points fixed by `g` are also fixed by `g⁻¹`  -/
MulAction.fixedBy_inv : ∀ (α : Type u_1) {G : Type u_2} [inst : Group G] [inst_1 : MulAction G α] (g : G),
  MulAction.fixedBy α g⁻¹ = MulAction.fixedBy α g
-- Mathlib.Topology.Instances.EReal.Lemmas
EReal.Tendsto.mul_const : ∀ {α : Type u_2} {f : Filter α} {m : α → EReal} {a b : EReal},
  Filter.Tendsto m f (nhds a) → a ≠ 0 ∨ b ≠ ⊥ → a ≠ 0 ∨ b ≠ ⊤ → Filter.Tendsto (fun x => m x * b) f (nhds (a * b))
-- Mathlib.Algebra.Homology.SingleHomology
HomologicalComplex.singleObjCyclesSelfIso_hom_singleObjOpcyclesSelfIso_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {ι : Type u_1} [inst_3 : DecidableEq ι] (c : ComplexShape ι) (j : ι)
  (A : C),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.singleObjCyclesSelfIso c j A).hom
      (HomologicalComplex.singleObjOpcyclesSelfIso c j A).hom =
    CategoryTheory.CategoryStruct.comp (((HomologicalComplex.single C c j).obj A).iCycles j)
      (((HomologicalComplex.single C c j).obj A).pOpcycles j)
-- Mathlib.Topology.Category.LightProfinite.Extend
/-- Given a sequential cone in `LightProfinite` consisting of finite sets,
we obtain a functor from the indexing category to `StructuredArrow c.pt toLightProfinite`.
 -/
LightProfinite.Extend.functor : {F : CategoryTheory.Functor ℕᵒᵖ FintypeCat} →
  (c : CategoryTheory.Limits.Cone (F.comp FintypeCat.toLightProfinite)) →
    CategoryTheory.Functor ℕᵒᵖ (CategoryTheory.StructuredArrow c.pt FintypeCat.toLightProfinite)
-- Mathlib.LinearAlgebra.Matrix.Circulant
Matrix.circulant_neg : ∀ {α : Type u_1} {n : Type u_3} [inst : Neg α] [inst_1 : Sub n] (v : n → α), Matrix.circulant (-v) = -Matrix.circulant v
-- Mathlib.LinearAlgebra.Matrix.StdBasis
Matrix.stdBasis_eq_single : ∀ (R : Type u_1) {m : Type u_2} {n : Type u_3} [inst : Fintype m] [inst_1 : Finite n] [inst_2 : Semiring R] (i : m)
  (j : n) [inst_3 : DecidableEq m] [inst_4 : DecidableEq n], (Matrix.stdBasis R m n) (i, j) = Matrix.single i j 1
-- Mathlib.Topology.Algebra.InfiniteSum.Constructions
/-- If a series `f` on `β × γ` has sum `a` and for each `b` the
restriction of `f` to `{b} × γ` has sum `g b`, then the series `g` has sum `a`.  -/
HasSum.prod_fiberwise : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] [ContinuousAdd α]
  [RegularSpace α] {f : β × γ → α} {g : β → α} {a : α},
  HasSum f a → (∀ (b : β), HasSum (fun c => f (b, c)) (g b)) → HasSum g a
-- Mathlib.Algebra.Ring.BooleanRing
toBoolRing_inf : ∀ {α : Type u_1} [inst : BooleanAlgebra α] (a b : α), toBoolRing (a ⊓ b) = toBoolRing a * toBoolRing b
-- Mathlib.Analysis.Normed.Operator.Extend
LinearMap.norm_extendOfNorm_apply_le : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_3} {Eₗ : Type u_4} {F : Type u_5} [inst : NormedDivisionRing 𝕜]
  [inst_1 : NormedDivisionRing 𝕜₂] {σ₁₂ : 𝕜 →+* 𝕜₂} [inst_2 : AddCommGroup E] [inst_3 : SeminormedAddCommGroup Eₗ]
  [inst_4 : NormedAddCommGroup F] [inst_5 : Module 𝕜 E] [inst_6 : Module 𝕜₂ F] [inst_7 : IsBoundedSMul 𝕜₂ F]
  [inst_8 : Module 𝕜 Eₗ] [inst_9 : IsBoundedSMul 𝕜 Eₗ] [inst_10 : CompleteSpace F] {f : E →ₛₗ[σ₁₂] F} {e : E →ₗ[𝕜] Eₗ},
  DenseRange ⇑e → ∀ (C : ℝ), (∀ (x : E), ‖f x‖ ≤ C * ‖e x‖) → ∀ (x : Eₗ), ‖(f.extendOfNorm e) x‖ ≤ C * ‖x‖
-- Mathlib.Data.Finmap
Finmap.singleton.eq_1 : ∀ {α : Type u} {β : α → Type v} (a : α) (b : β a), Finmap.singleton a b = (AList.singleton a b).toFinmap
-- Init.Data.Iterators.Lemmas.Combinators.Attach
Std.Iter.unattach_toArray_attachWith : ∀ {α β : Type u_1} {P : β → Prop} [inst : Std.Iterator α Id β] {it : Std.Iter β}
  {hP : ∀ (out : β), it.IsPlausibleIndirectOutput out → P out} [Std.Iterators.Finite α Id],
  (it.attachWith P hP).toListRev.unattach = it.toListRev
-- Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic
IsLocalRing.ringJacobson_eq_maximalIdeal : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsLocalRing R], Ring.jacobson R = IsLocalRing.maximalIdeal R
-- Aesop.Rule
Aesop.RegularRule.unsafe.sizeOf_spec : ∀ (r : Aesop.UnsafeRule), sizeOf (Aesop.RegularRule.unsafe r) = 1 + sizeOf r
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
TensorProduct.instInnerProductSpace : {𝕜 : Type u_1} →
  {E : Type u_2} →
    {F : Type u_3} →
      [inst : RCLike 𝕜] →
        [inst_1 : NormedAddCommGroup E] →
          [inst_2 : InnerProductSpace 𝕜 E] →
            [inst_3 : NormedAddCommGroup F] →
              [inst_4 : InnerProductSpace 𝕜 F] → InnerProductSpace 𝕜 (TensorProduct 𝕜 E F)
-- Mathlib.Data.Setoid.Basic
Setoid.comm : ∀ {α : Type u_1} [inst : Setoid α] {x y : α}, x ≈ y ↔ y ≈ x
-- Mathlib.LinearAlgebra.AffineSpace.Combination
/-- `weightedVSub` gives the sum of the results of subtracting any
base point, when the sum of the weights is 0.  -/
Finset.weightedVSub_eq_weightedVSubOfPoint_of_sum_eq_zero : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) (w : ι → k) (p : ι → P),
  ∑ i ∈ s, w i = 0 → ∀ (b : P), (s.weightedVSub p) w = (s.weightedVSubOfPoint p b) w
-- Mathlib.Data.Sym.Sym2
/-- The universal property of `Sym2`; symmetric functions of two arguments are equivalent to
functions from `Sym2`. Note that when `β` is `Prop`, it can sometimes be more convenient to use
`Sym2.fromRel` instead.  -/
Sym2.lift : {α : Type u_1} → {β : Type u_2} → { f // ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁ } ≃ (Sym2 α → β)
-- Mathlib.Order.Filter.AtTopBot.Field
/-- If `f` tends to infinity along a nontrivial filter `l`, then
`fun x ↦ f x * r` tends to infinity if and only if `0 < r`.  -/
Filter.tendsto_mul_const_atTop_iff_pos : ∀ {α : Type u_1} {β : Type u_2} [inst : Semifield α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {l : Filter β}
  {f : β → α} {r : α} [l.NeBot],
  Filter.Tendsto f l Filter.atTop → (Filter.Tendsto (fun x => f x * r) l Filter.atTop ↔ 0 < r)
-- Std.Data.HashMap.Lemmas
Std.HashMap.getElem?_inter_of_not_mem_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α}, k ∉ m₁ → (m₁ ∩ m₂)[k]? = none
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
CategoryTheory.Limits.CatCospanTransform.id_whiskerLeft_assoc : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆}
  [inst : CategoryTheory.Category.{v₁, u₁} A] [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] [inst_4 : CategoryTheory.Category.{v₅, u₅} B']
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'}
  {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F G F' G'} (η : ψ ⟶ ψ')
  {Z : CategoryTheory.Limits.CatCospanTransform F G F' G'}
  (h : (CategoryTheory.Limits.CatCospanTransform.id F G).comp ψ' ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.CatCospanTransformMorphism.whiskerLeft (CategoryTheory.Limits.CatCospanTransform.id F G) η)
      h =
    CategoryTheory.CategoryStruct.comp ψ.leftUnitor.hom
      (CategoryTheory.CategoryStruct.comp η (CategoryTheory.CategoryStruct.comp ψ'.leftUnitor.inv h))
-- Batteries.Control.Lemmas
StateT.run_throw : ∀ {m : Type u_1 → Type u_2} {ε : Type u_3} {σ α : Type u_1} [inst : Monad m] [inst_1 : MonadExceptOf ε m] (e : ε)
  (s : σ),
  (throw e).run s = do
    let a ← throw e
    pure (a, s)
-- Mathlib.RingTheory.Localization.BaseChange
LocalizedModule.isBaseChange : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) (M : Type u_3) [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M], IsBaseChange (Localization S) (LocalizedModule.mkLinearMap S M)
-- Aesop.Frontend.Extension
Aesop.Frontend.declareRuleSet : {m : Type → Type} → [Monad m] → [Lean.MonadError m] → [MonadLiftT IO m] → Aesop.RuleSetName → Bool → m Unit
-- Mathlib.Geometry.Euclidean.Sphere.Power
/-- The power of a point with respect to a sphere. For a point and a sphere,
this is defined as the square of the distance from the point to the center
minus the square of the radius. This value is positive if the point is outside
the sphere, negative if inside, and zero if on the sphere.  -/
EuclideanGeometry.Sphere.power : {P : Type u_2} → [inst : MetricSpace P] → EuclideanGeometry.Sphere P → P → ℝ
-- Mathlib.Data.Num.Basic
/-- Subtraction of two `Num`s, where if `a < b`, `a - b = 0`.  -/
Num.sub : Num → Num → Num
-- Mathlib.Algebra.Order.Group.OrderIso
OrderIso.addRight_symm : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LE α] [inst_2 : AddRightMono α] (a : α),
  (OrderIso.addRight a).symm = OrderIso.addRight (-a)
-- Mathlib.RingTheory.AdicCompletion.Algebra
/-- `AdicCompletion I R` is an `R`-subalgebra of `∀ n, R ⧸ (I ^ n • ⊤ : Ideal R)`.  -/
AdicCompletion.subalgebra : {R : Type u_1} → [inst : CommRing R] → (I : Ideal R) → Subalgebra R ((n : ℕ) → R ⧸ I ^ n • ⊤)
-- Mathlib.RingTheory.Flat.Equalizer
LinearMap.tensorKerEquiv_apply : ∀ {R : Type u_1} (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (M : Type u_3)
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : Module S M] [inst_6 : IsScalarTower R S M] {N : Type u_4}
  {P : Type u_5} [inst_7 : AddCommGroup N] [inst_8 : AddCommGroup P] [inst_9 : Module R N] [inst_10 : Module R P]
  (f : N →ₗ[R] P) [inst_11 : Module.Flat R M] (x : TensorProduct R M ↥f.ker),
  (LinearMap.tensorKerEquiv S M f) x = (LinearMap.tensorKer S M f) x
-- Mathlib.ModelTheory.Semantics
_private.Mathlib.ModelTheory.Semantics.0.FirstOrder.Language.BoundedFormula.restrictFreeVar.match_1.eq_2 : ∀ {L : FirstOrder.Language} {α : Type u_3} {β : Type u_5} [inst : DecidableEq α]
  (motive : (x : ℕ) → (x_1 : L.BoundedFormula α x) → (↥x_1.freeVarFinset → β) → Sort u_4) (_n : ℕ)
  (t₁ t₂ : L.Term (α ⊕ Fin _n)) (f : ↥(FirstOrder.Language.BoundedFormula.equal t₁ t₂).freeVarFinset → β)
  (h_1 :
    (_n : ℕ) →
      (_f : ↥FirstOrder.Language.BoundedFormula.falsum.freeVarFinset → β) →
        motive _n FirstOrder.Language.BoundedFormula.falsum _f)
  (h_2 :
    (_n : ℕ) →
      (t₁ t₂ : L.Term (α ⊕ Fin _n)) →
        (f : ↥(FirstOrder.Language.BoundedFormula.equal t₁ t₂).freeVarFinset → β) →
          motive _n (FirstOrder.Language.BoundedFormula.equal t₁ t₂) f)
  (h_3 :
    (_n l : ℕ) →
      (R : L.Relations l) →
        (ts : Fin l → L.Term (α ⊕ Fin _n)) →
          (f : ↥(FirstOrder.Language.BoundedFormula.rel R ts).freeVarFinset → β) →
            motive _n (FirstOrder.Language.BoundedFormula.rel R ts) f)
  (h_4 : (_n : ℕ) → (φ₁ φ₂ : L.BoundedFormula α _n) → (f : ↥(φ₁.imp φ₂).freeVarFinset → β) → motive _n (φ₁.imp φ₂) f)
  (h_5 : (_n : ℕ) → (φ : L.BoundedFormula α (_n + 1)) → (f : ↥φ.all.freeVarFinset → β) → motive _n φ.all f),
  (match _n, FirstOrder.Language.BoundedFormula.equal t₁ t₂, f with
    | _n, FirstOrder.Language.BoundedFormula.falsum, _f => h_1 _n _f
    | _n, FirstOrder.Language.BoundedFormula.equal t₁ t₂, f => h_2 _n t₁ t₂ f
    | _n, FirstOrder.Language.BoundedFormula.rel R ts, f => h_3 _n l R ts f
    | _n, φ₁.imp φ₂, f => h_4 _n φ₁ φ₂ f
    | _n, φ.all, f => h_5 _n φ f) =
    h_2 _n t₁ t₂ f
-- Std.Do.PostCond
/-- The assertions in this monad may mention the current value of a state of type `σ`, and
postconditions may mention the state's final value.
 -/
Std.Do.PostShape.arg : Type u → Std.Do.PostShape → Std.Do.PostShape
-- Lean.Meta.Offset
_private.Lean.Meta.Offset.0.Lean.Meta.evalNat.evalPow : Lean.Expr → Lean.Expr → OptionT Lean.MetaM ℕ
-- Mathlib.Algebra.Order.Ring.StandardPart
ArchimedeanClass.FiniteElement.not_isUnit_iff_mk_pos : ∀ {K : Type u_1} [inst : LinearOrder K] [inst_1 : Field K] [inst_2 : IsOrderedRing K]
  {x : ArchimedeanClass.FiniteElement K}, ¬IsUnit x ↔ 0 < ArchimedeanClass.mk ↑x
-- Mathlib.Order.Filter.Cocardinal
Filter.eventually_cocardinal : ∀ {α : Type u} {c : Cardinal.{u}} {hreg : c.IsRegular} {p : α → Prop},
  (∀ᶠ (x : α) in Filter.cocardinal α hreg, p x) ↔ Cardinal.mk ↑{x | ¬p x} < c
-- Mathlib.CategoryTheory.Functor.Derived.RightDerived
CategoryTheory.Functor.rightDerivedNatTrans_fac : ∀ {C : Type u_1} {D : Type u_3} {H : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} D] [inst_2 : CategoryTheory.Category.{v_5, u_2} H]
  (RF RF' : CategoryTheory.Functor D H) {F F' : CategoryTheory.Functor C H} {L : CategoryTheory.Functor C D}
  (α : F ⟶ L.comp RF) (α' : F' ⟶ L.comp RF') (W : CategoryTheory.MorphismProperty C) [inst_3 : L.IsLocalization W]
  [inst_4 : RF.IsRightDerivedFunctor α W] (τ : F ⟶ F'),
  CategoryTheory.CategoryStruct.comp α (L.whiskerLeft (RF.rightDerivedNatTrans RF' α α' W τ)) =
    CategoryTheory.CategoryStruct.comp τ α'