mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
/-- For any `I : Ideal A`, not necessarily homogeneous, `I.homogeneousCore' 𝒜`
is the largest homogeneous ideal of `A` contained in `I`.  -/
Ideal.homogeneousCore : {ι : Type u_1} →
  {σ : Type u_2} →
    {A : Type u_3} →
      [inst : Semiring A] →
        [inst_1 : SetLike σ A] →
          [inst_2 : AddSubmonoidClass σ A] →
            (𝒜 : ι → σ) →
              [inst_3 : DecidableEq ι] → [inst_4 : AddMonoid ι] → [inst_5 : GradedRing 𝒜] → Ideal A → HomogeneousIdeal 𝒜
-- Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Polynomial.trdeg_of_isDomain : ∀ {R : Type u_1} [inst : CommRing R] [IsDomain R], Algebra.trdeg R (Polynomial R) = 1
-- Mathlib.Data.ENNReal.Operations
ENNReal.add_iInf₂ : ∀ {ι : Sort u_1} {a : ENNReal} {κ : ι → Sort u_2} (f : (i : ι) → κ i → ENNReal),
  a + ⨅ i, ⨅ j, f i j = ⨅ i, ⨅ j, a + f i j
-- Lean.Util.ParamMinimizer
_private.Lean.Util.ParamMinimizer.0.Lean.Util.ParamMinimizer.State.added : Lean.Util.ParamMinimizer.State✝ → Array ℕ
-- Mathlib.Data.Finsupp.Weight
Finsupp.weight_single_index : ∀ {σ : Type u_1} {M : Type u_2} {R : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : DecidableEq σ] (s : σ) (c : M) (f : σ →₀ R), (Finsupp.weight (Pi.single s c)) f = f s • c
-- Mathlib.Data.Finset.Sups
Finset.image_inf_product : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SemilatticeInf α] (s t : Finset α),
  Finset.image (Function.uncurry fun x1 x2 => x1 ⊓ x2) (s ×ˢ t) = s ⊼ t
-- Mathlib.Data.Finset.Card
Finset.card_sdiff_le_card_sdiff_iff : ∀ {α : Type u_1} {s t : Finset α} [inst : DecidableEq α], (s \ t).card ≤ (t \ s).card ↔ s.card ≤ t.card
-- Mathlib.Order.Filter.AtTopBot.Field
/-- If `f` tends to infinity along a nontrivial filter `l`, then
`x ↦ f x * r` tends to infinity if and only if `0 < r`.  -/
Filter.tendsto_div_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)
-- Mathlib.Order.CompleteLattice.Basic
iInf_congr_Prop : ∀ {α : Type u_1} [inst : InfSet α] {p q : Prop} {f₁ : p → α} {f₂ : q → α} (pq : p ↔ q),
  (∀ (x : q), f₁ ⋯ = f₂ x) → iInf f₁ = iInf f₂
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.keys_filter_key : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} {f : α → Bool} (h : t.WF),
  (Std.DTreeMap.Internal.Impl.filter (fun k x => f k) t ⋯).impl.keys = List.filter f t.keys
-- Mathlib.Data.Real.ConjExponents
Real.HolderTriple.nonneg : ∀ {p q r : ℝ}, p.HolderTriple q r → 0 ≤ p
-- Mathlib.Analysis.Normed.Ring.Basic
NonUnitalNormedRing.toNorm : {α : Type u_5} → [self : NonUnitalNormedRing α] → Norm α
-- Mathlib.Analysis.Normed.Order.UpperLower
IsLowerSet.thickening : ∀ {α : Type u_1} [inst : NormedAddCommGroup α] [inst_1 : Preorder α] [IsOrderedAddMonoid α] {s : Set α},
  IsLowerSet s → ∀ (ε : ℝ), IsLowerSet (Metric.thickening ε s)
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
MeasureTheory.SimpleFunc.extend.congr_simp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  (f₁ f₁_1 : MeasureTheory.SimpleFunc α γ),
  f₁ = f₁_1 →
    ∀ (g g_1 : α → β) (e_g : g = g_1) (hg : MeasurableEmbedding g) (f₂ f₂_1 : MeasureTheory.SimpleFunc β γ),
      f₂ = f₂_1 → f₁.extend g hg f₂ = f₁_1.extend g_1 ⋯ f₂_1
-- Mathlib.Topology.Inseparable
stableUnderGeneralization_sInter : ∀ {X : Type u_1} [inst : TopologicalSpace X] (S : Set (Set X)),
  (∀ s ∈ S, StableUnderGeneralization s) → StableUnderGeneralization (⋂₀ S)
-- Mathlib.Order.Bounds.Basic
isGLB_empty : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : OrderTop α], IsGLB ∅ ⊤
-- Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
Measurable.quasiMeasurePreserving : ∀ {α : Type u_1} {β : Type u_2} {mβ : MeasurableSpace β} {f : α → β} {_m0 : MeasurableSpace α},
  Measurable f →
    ∀ (μ : MeasureTheory.Measure α), MeasureTheory.Measure.QuasiMeasurePreserving f μ (MeasureTheory.Measure.map f μ)
-- Mathlib.RingTheory.Coalgebra.Basic
LinearMap.diag.eq_1 : ∀ {R : Type u} {ι : Type x} [inst : Semiring R] {φ : ι → Type i} [inst_1 : (i : ι) → AddCommMonoid (φ i)]
  [inst_2 : (i : ι) → Module R (φ i)] [inst_3 : DecidableEq ι] (i j : ι),
  LinearMap.diag i j = Function.update 0 i LinearMap.id j
-- Mathlib.Topology.OpenPartialHomeomorph.Defs
OpenPartialHomeomorph.coe_mk_symm : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (e : PartialEquiv X Y)
  (h₁ : ContinuousOn (↑e) e.source) (h₂ : ContinuousOn e.invFun e.target)
  (h₃ : IsOpen { toPartialEquiv := e, continuousOn_toFun := h₁, continuousOn_invFun := h₂ }.source)
  (h₄ : IsOpen { toPartialEquiv := e, continuousOn_toFun := h₁, continuousOn_invFun := h₂ }.target),
  ↑{ toPartialEquiv := e, continuousOn_toFun := h₁, continuousOn_invFun := h₂, open_source := h₃,
          open_target := h₄ }.symm =
    ↑e.symm
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Ioo_union_Ico_eq_Ioo : ∀ {α : Type u_1} [inst : LinearOrder α] {a b c : α}, a < b → b ≤ c → Set.Ioo a b ∪ Set.Ico b c = Set.Ioo a c
-- Mathlib.Order.SuccPred.Limit
Order.isSuccLimitRecOn_of_isSuccLimit : ∀ {α : Type u_1} {b : α} {motive : α → Sort u_2} [inst : PartialOrder α] [inst_1 : SuccOrder α]
  (isMin : (a : α) → IsMin a → motive a) (succ : (a : α) → ¬IsMax a → motive (Order.succ a))
  (isSuccLimit : (a : α) → Order.IsSuccLimit a → motive a) (hb : Order.IsSuccLimit b),
  Order.isSuccLimitRecOn b isMin succ isSuccLimit = isSuccLimit b hb
-- Mathlib.Combinatorics.HalesJewett
Combinatorics.Subspace.IsMono.reindex : ∀ {η : Type u_5} {α : Type u_6} {ι : Type u_7} {κ : Type u_8} {l : Combinatorics.Subspace η α ι} {η' : Type u_9}
  {α' : Type u_10} {ι' : Type u_11} {eη : η ≃ η'} {eα : α ≃ α'} {eι : ι ≃ ι'} {C : (ι → α) → κ},
  Combinatorics.Subspace.IsMono C l →
    Combinatorics.Subspace.IsMono (fun x => C (⇑eα.symm ∘ x ∘ ⇑eι)) (l.reindex eη eα eι)
-- Mathlib.Data.List.Fold
/-- **Alias** of `List.foldl_cons_eq_apply_foldl`. -/
List.foldl_assoc_comm_cons : ∀ {α : Type u_1} {β : Type u_2} {l : List α} {v : β → α → β} {a : α} {b : β} [hv : RightCommutative v],
  List.foldl v b (a :: l) = v (List.foldl v b l) a
-- Mathlib.Tactic.CategoryTheory.Coherence
Mathlib.Tactic.Coherence.insert_id_rhs : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : C} (f g : X ⟶ Y),
  f = CategoryTheory.CategoryStruct.comp g (CategoryTheory.CategoryStruct.id Y) → f = g
-- Mathlib.Algebra.Group.Idempotent
IsIdempotentElem.mul : ∀ {S : Type u_3} [inst : CommSemigroup S] {a b : S}, IsIdempotentElem a → IsIdempotentElem b → IsIdempotentElem (a * b)
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.getD_eq_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  {k fallback : α}, k ∈ t → t.getD k fallback = k
-- Mathlib.Algebra.Module.Torsion.Basic
isAddTorsion_iff_isTorsion_int : ∀ {M : Type u_2} [inst : AddCommGroup M], IsAddTorsion M ↔ Module.IsTorsion ℤ M
-- Mathlib.Topology.Algebra.Module.Complement
Submodule.ClosedComplemented.isTopCompl_complement : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_2} [inst_1 : TopologicalSpace M] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] {p : Submodule R M} (h : p.ClosedComplemented), Submodule.IsTopCompl p h.complement
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
/-- **Alias** of the forward direction of `sub_lt_iff_lt_add`. -/
lt_add_of_sub_right_lt : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LT α] [AddRightStrictMono α] {a b c : α}, a - c < b → a < b + c
-- Mathlib.Analysis.Fourier.Notation
FourierPair.mk : ∀ {E : Type u_5} {F : Type u_6} [inst : FourierTransform E F] [inst_1 : FourierTransformInv F E],
  (∀ (f : E), FourierTransformInv.fourierInv (FourierTransform.fourier f) = f) → FourierPair E F
-- Init.Data.List.Lemmas
List.exists_mem_nil : ∀ {α : Type u_1} (p : α → Prop), ¬∃ x, ∃ (_ : x ∈ []), p x
-- Init.Data.Fin.Fold
Fin.foldrM_pure : ∀ {m : Type u_1 → Type u_2} {α : Type u_1} {x : α} [inst : Monad m] [LawfulMonad m] {n : ℕ} {f : Fin n → α → α},
  Fin.foldrM n (fun i x => pure (f i x)) x = pure (Fin.foldr n f x)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.CoordinateRing.coe_norm_smul_basis : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Affine R} (p q : Polynomial R),
  (AdjoinRoot.of W'.polynomial)
      ((Algebra.norm (Polynomial R)) (p • 1 + q • (WeierstrassCurve.Affine.CoordinateRing.mk W') Polynomial.X)) =
    (WeierstrassCurve.Affine.CoordinateRing.mk W')
      ((Polynomial.C p + Polynomial.C q * Polynomial.X) *
        (Polynomial.C p +
          Polynomial.C q * (-Polynomial.X - Polynomial.C (Polynomial.C W'.a₁ * Polynomial.X + Polynomial.C W'.a₃))))
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Implementation
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.mk.sizeOf_spec : ∀ {numVarsSucc : ℕ} (clauses : Array (Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause numVarsSucc)))
  (rupUnits ratUnits : Array (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin numVarsSucc)))
  (assignments : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment),
  sizeOf { clauses := clauses, rupUnits := rupUnits, ratUnits := ratUnits, assignments := assignments } =
    1 + sizeOf clauses + sizeOf rupUnits + sizeOf ratUnits + sizeOf assignments
-- Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter
CategoryTheory.SimplicialObject.σ_δ₀Iter'_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (X : CategoryTheory.SimplicialObject C) (i : ℕ) {n m : ℕ}
  (j : Fin (m + 1)) (j' : Fin (n + 1)) (hi' : autoParam (n + i = m) CategoryTheory.SimplicialObject.σ_δ₀Iter'._auto_1),
  autoParam (↑j = ↑j' + i) CategoryTheory.SimplicialObject.σ_δ₀Iter'._auto_3 →
    ∀ {Z : C} (h : X.obj (Opposite.op { len := n + 1 }) ⟶ Z),
      CategoryTheory.CategoryStruct.comp (X.σ j) (CategoryTheory.CategoryStruct.comp (X.δ₀Iter i ⋯) h) =
        CategoryTheory.CategoryStruct.comp (X.δ₀Iter i hi') (CategoryTheory.CategoryStruct.comp (X.σ j') h)
-- Mathlib.RingTheory.PowerSeries.Substitution
PowerSeries.HasSubst.X : ∀ {τ : Type u_3} {S : Type u_4} [inst : CommRing S] (t : τ), PowerSeries.HasSubst (MvPowerSeries.X t)
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.instAdd : {ι : Type u_1} →
  {A : Type u_2} →
    {σ : Type u_3} →
      [inst : CommRing A] →
        [inst_1 : SetLike σ A] →
          [inst_2 : AddSubgroupClass σ A] →
            [inst_3 : AddCommMonoid ι] →
              [inst_4 : DecidableEq ι] →
                {𝒜 : ι → σ} → [GradedRing 𝒜] → (x : Submonoid A) → Add (HomogeneousLocalization 𝒜 x)
-- Init.Data.Int.LemmasAux
/-- A corollary of |s| ≤ x, and |t| ≤ y, then |s * t| ≤ x * y,
 -/
Int.neg_mul_le_mul : ∀ {x y : ℤ} {s t : ℕ}, -↑s ≤ x → x < ↑s → -↑t ≤ y → y < ↑t → -(↑s * ↑t) ≤ x * y
-- Std.Time.Format.DateFormat
/-- Full quarter names (4 elements, index 0 = 1st quarter).
 -/
Std.Time.DateFormatSymbols.quarterLong : Std.Time.DateFormatSymbols → Vector String 4
-- Mathlib.Order.Category.BddDistLat
BddDistLat.instCategory : CategoryTheory.Category.{u, u + 1} BddDistLat
-- Mathlib.RingTheory.Polynomial.Hermite.Basic
Polynomial.hermite_zero : Polynomial.hermite 0 = Polynomial.C 1
-- Mathlib.Topology.Homeomorph.Lemmas
/-- If `ι` has a unique element, then `ι → X` is homeomorphic to `X`.  -/
Homeomorph.funUnique : (ι : Type u_7) → (X : Type u_8) → [Unique ι] → [inst : TopologicalSpace X] → (ι → X) ≃ₜ X
-- Std.Internal.UV.UDP
/-- Associates the UDP socket with the given address and port, so every message sent by this socket is
automatically sent to that destination.
 -/
Std.Internal.UV.UDP.Socket.connect : Std.Internal.UV.UDP.Socket → Std.Net.SocketAddress → IO Unit
-- Mathlib.CategoryTheory.Bicategory.Functor.Cat.ObjectProperty
CategoryTheory.Pseudofunctor.ObjectProperty.ι_app_toFunctor : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat}
  (P : F.ObjectProperty) [inst_1 : P.IsClosedUnderMapObj] (X : B), (P.ι.app X).toFunctor = (P.prop X).ι
-- Init.Data.List.ToArray
_private.Init.Data.List.ToArray.0.Array.leftpad.eq_1 : ∀ {α : Type u} (n : ℕ) (a : α) (xs : Array α), Array.leftpad n a xs = Array.replicate (n - xs.size) a ++ xs
-- Batteries.Tactic.HelpCmd
_private.Batteries.Tactic.HelpCmd.0.Batteries.Tactic.elabHelpCat : Option Lean.Syntax → Lean.Ident → Option String → Lean.Elab.Command.CommandElabM Unit
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.mem_modify : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α], t.WF → ∀ {k k' : α} {f : β k → β k}, k' ∈ Std.DTreeMap.Internal.Impl.modify k f t ↔ k' ∈ t
-- Mathlib.CategoryTheory.Triangulated.Functor
/-- The image of an octahedron by a triangulated functor.  -/
CategoryTheory.Triangulated.Octahedron.map : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        [inst_2 : CategoryTheory.HasShift C ℤ] →
          [inst_3 : CategoryTheory.HasShift D ℤ] →
            [inst_4 : CategoryTheory.Limits.HasZeroObject C] →
              [inst_5 : CategoryTheory.Limits.HasZeroObject D] →
                [inst_6 : CategoryTheory.Preadditive C] →
                  [inst_7 : CategoryTheory.Preadditive D] →
                    [inst_8 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
                      [inst_9 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] →
                        [inst_10 : CategoryTheory.Pretriangulated C] →
                          [inst_11 : CategoryTheory.Pretriangulated D] →
                            {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} →
                              {u₁₂ : X₁ ⟶ X₂} →
                                {u₂₃ : X₂ ⟶ X₃} →
                                  {u₁₃ : X₁ ⟶ X₃} →
                                    {comm : CategoryTheory.CategoryStruct.comp u₁₂ u₂₃ = u₁₃} →
                                      {v₁₂ : X₂ ⟶ Z₁₂} →
                                        {w₁₂ : Z₁₂ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁} →
                                          {h₁₂ :
                                              CategoryTheory.Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈
                                                CategoryTheory.Pretriangulated.distinguishedTriangles} →
                                            {v₂₃ : X₃ ⟶ Z₂₃} →
                                              {w₂₃ : Z₂₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₂} →
                                                {h₂₃ :
                                                    CategoryTheory.Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈
                                                      CategoryTheory.Pretriangulated.distinguishedTriangles} →
                                                  {v₁₃ : X₃ ⟶ Z₁₃} →
                                                    {w₁₃ : Z₁₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁} →
                                                      {h₁₃ :
                                                          CategoryTheory.Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈
                                                            CategoryTheory.Pretriangulated.distinguishedTriangles} →
                                                        CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃ →
                                                          (F : CategoryTheory.Functor C D) →
                                                            [inst_12 : F.CommShift ℤ] →
                                                              [inst_13 : F.IsTriangulated] →
                                                                CategoryTheory.Triangulated.Octahedron ⋯ ⋯ ⋯ ⋯
-- Mathlib.Data.Set.Basic
Set.inter_nonempty_iff_exists_left : ∀ {α : Type u} {s t : Set α}, (s ∩ t).Nonempty ↔ ∃ x ∈ s, x ∈ t
-- Mathlib.Data.Multiset.Find
Multiset.find?_some : ∀ {α : Type u_1} (p : α → Prop) [inst : DecidablePred p] {a : α} {s : Multiset α} {hp : {x | x ∈ s ∧ p x}.Subsingleton},
  Multiset.find? p s hp = some a → p a
-- Std.Async.Basic
/-- Runs all computations concurrently and returns the result of the first one to finish.
All other results are lost, and the tasks are not cancelled, so they'll continue their execution
until the end.
 -/
Std.Async.BaseAsync.raceAll : {α : Type} →
  {c : Type u_1} →
    [Inhabited α] →
      [ForM Std.Async.BaseAsync c (Std.Async.BaseAsync α)] →
        c → optParam Task.Priority Task.Priority.default → Std.Async.BaseAsync α
-- Mathlib.GroupTheory.Congruence.Defs
/-- Congruence relations are reflexive.  -/
Con.refl : ∀ {M : Type u_1} [inst : Mul M] (c : Con M) (x : M), c x x
-- Mathlib.GroupTheory.Index
Subgroup.finiteIndex_iff_finite_quotient : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G}, H.FiniteIndex ↔ Finite (G ⧸ H)
-- Lean.Meta.Tactic.Grind.Core
_private.Lean.Meta.Tactic.Grind.Core.0.Lean.Meta.Grind.addEqStep.updateRoots : Lean.Expr → Lean.Expr → Lean.Meta.Grind.GoalM Unit
-- Std.Tactic.BVDecide.LRAT.Internal.PosFin
Std.Tactic.BVDecide.LRAT.Internal.instCoeOutPosFinNat : {n : ℕ} → CoeOut (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) ℕ
-- Mathlib.Combinatorics.Enumerative.DoubleCounting
Fintype.card_le_card_of_leftTotal_unique : ∀ {α : Type u_2} {β : Type u_3} [inst : Fintype α] [inst_1 : Fintype β] {r : α → β → Prop},
  Relator.LeftTotal r → Relator.LeftUnique r → Fintype.card α ≤ Fintype.card β
-- Mathlib.Lean.Meta.RefinedDiscrTree.Basic
/-- A lambda function.  -/
Lean.Meta.RefinedDiscrTree.Key.lam : Lean.Meta.RefinedDiscrTree.Key
-- Mathlib.Analysis.Calculus.Gradient.Basic
gradient_eq_zero_of_not_differentiableAt : ∀ {𝕜 : Type u_1} {F : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup F] [inst_2 : InnerProductSpace 𝕜 F]
  [inst_3 : CompleteSpace F] {f : F → 𝕜} {x : F}, ¬DifferentiableAt 𝕜 f x → gradient f x = 0
-- Lean.Elab.InfoTree.Types
Lean.Elab.Info.ofCustomInfo.sizeOf_spec : ∀ (i : Lean.Elab.CustomInfo), sizeOf (Lean.Elab.Info.ofCustomInfo i) = 1 + sizeOf i
-- Mathlib.Topology.Algebra.ProperAction.Basic
/-- If `G` acts on `X` properly, the set `s • t` is closed when `s : Set G` is *closed* and
`t : Set X` is *compact*.

See also `IsClosed.smul_left_of_isCompact` for a version with the assumptions on `s` and `t`
reversed.  -/
IsClosed.smul_right_of_isCompact : ∀ {G : Type u_1} {X : Type u_2} [inst : Group G] [inst_1 : MulAction G X] [inst_2 : TopologicalSpace G]
  [inst_3 : TopologicalSpace X] [ProperSMul G X] {s : Set G} {t : Set X}, IsClosed s → IsCompact t → IsClosed (s • t)
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
ContinuousMultilinearMap.smulRightL_apply : ∀ {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)]
  [inst_3 : SeminormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] [inst_5 : Fintype ι]
  (f : ContinuousMultilinearMap 𝕜 E 𝕜) (z : G), ((ContinuousMultilinearMap.smulRightL 𝕜 E G) f) z = f.smulRight z
-- Mathlib.Order.Interval.Finset.Defs
WithBot.bot_mem_insertBot : ∀ {α : Type u_1} {s : Finset α}, ⊥ ∈ WithBot.insertBot s
-- Std.Do.WP.SimpLemmas
Std.Do.WP.modifyThe_MonadStateOf : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {σ : Type u} {Q : Std.Do.PostCond PUnit.{u + 1} ps}
  [inst : Std.Do.WP m ps] [inst_1 : MonadStateOf σ m] (f : σ → σ),
  (Std.Do.wp (modifyThe σ f)).apply Q = (Std.Do.wp (MonadStateOf.modifyGet fun s => (PUnit.unit, f s))).apply Q
-- Mathlib.Tactic.GCongr.Core
/-- `mainSubgoals` are the subgoals on which `gcongr` will be recursively called.  -/
Mathlib.Tactic.GCongr.GCongrLemma.mainSubgoals : Mathlib.Tactic.GCongr.GCongrLemma → Array Mathlib.Tactic.GCongr.GCongrHyp
-- Mathlib.LinearAlgebra.Dual.Lemmas
Module.eval_ker : ∀ (K : Type uK) (V : Type uV) [inst : CommSemiring K] [inst_1 : AddCommMonoid V] [inst_2 : Module K V]
  [Module.Projective K V], (Module.Dual.eval K V).ker = ⊥
-- Init.Data.Range.Polymorphic.IntLemmas
Int.getElem?_toArray_rco_eq_none_iff : ∀ {m n : ℤ} {i : ℕ}, (m...n).toArray[i]? = none ↔ (n - m).toNat ≤ i
-- Mathlib.Order.SuccPred.Tree
/-- The predecessor relationship should be archimedean.  -/
RootedTree.isPredArchimedean : ∀ (self : RootedTree), IsPredArchimedean ↑self
-- Mathlib.Topology.VectorBundle.Basic
VectorBundleCore.toFiberBundleCore_baseSet : ∀ {R : Type u_1} {B : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField R] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace R F] [inst_3 : TopologicalSpace B] {ι : Type u_5} (Z : VectorBundleCore R B F ι),
  Z.toFiberBundleCore.baseSet = Z.baseSet
-- Mathlib.Algebra.Category.MonCat.Adjunctions
MonCat.adjoinOneAdj.eq_1 : MonCat.adjoinOneAdj =
  CategoryTheory.Adjunction.mkOfHomEquiv
    {
      homEquiv := fun X Y =>
        CategoryTheory.ConcreteCategory.homEquiv.trans
          (WithOne.lift.symm.trans CategoryTheory.ConcreteCategory.homEquiv.symm),
      homEquiv_naturality_left_symm := @MonCat.adjoinOneAdj._proof_1,
      homEquiv_naturality_right := @MonCat.adjoinOneAdj._proof_2 }
-- Mathlib.Data.Set.Image
Set.disjoint_range_inl_image_inr : ∀ {α : Type u_1} {β : Type u_2} {v : Set β}, Disjoint (Set.range Sum.inl) (Sum.inr '' v)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
/-- For `f : 𝕜 → 𝕜` continuous on a set `s` for which `f 0 = 0`, `cfcₙ f` is continuous on the
set of `a : A` satisfying the predicate `p` (associated to `𝕜`) and whose `𝕜`-quasispectrum is
contained in `s`.  -/
continuousOn_cfcₙ : ∀ {𝕜 : Type u_2} (A : Type u_3) {p : A → Prop} [inst : RCLike 𝕜] [inst_1 : NonUnitalNormedRing A] [inst_2 : StarRing A]
  [inst_3 : NormedSpace 𝕜 A] [inst_4 : IsScalarTower 𝕜 A A] [inst_5 : SMulCommClass 𝕜 A A] [ContinuousStar A]
  [inst_7 : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p] {s : Set 𝕜},
  IsCompact s →
    ∀ (f : 𝕜 → 𝕜),
      autoParam (ContinuousOn f s) continuousOn_cfcₙ._auto_1 →
        autoParam (f 0 = 0) continuousOn_cfcₙ._auto_3 →
          ContinuousOn (fun x => cfcₙ f x) {a | p a ∧ quasispectrum 𝕜 a ⊆ s}
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
SemimoduleCat.MonoidalCategory.rightUnitor_naturality : ∀ {R : Type u} [inst : CommSemiring R] {M N : SemimoduleCat R} (f : M ⟶ N),
  CategoryTheory.CategoryStruct.comp
      (SemimoduleCat.MonoidalCategory.tensorHom f (CategoryTheory.CategoryStruct.id (SemimoduleCat.of R R)))
      (SemimoduleCat.MonoidalCategory.rightUnitor N).hom =
    CategoryTheory.CategoryStruct.comp (SemimoduleCat.MonoidalCategory.rightUnitor M).hom f
-- Mathlib.LinearAlgebra.AffineSpace.Ordered
lineMap_le_lineMap_iff_of_lt : ∀ {k : Type u_1} {E : Type u_2} [inst : Field k] [inst_1 : LinearOrder k] [IsStrictOrderedRing k]
  [inst_3 : AddCommGroup E] [inst_4 : PartialOrder E] [IsOrderedAddMonoid E] [inst_6 : Module k E]
  [IsStrictOrderedModule k E] [PosSMulReflectLE k E] {a b : E} {r r' : k},
  r < r' → ((AffineMap.lineMap a b) r ≤ (AffineMap.lineMap a b) r' ↔ a ≤ b)
-- Mathlib.Algebra.Star.Unitary
Unitary.mul_inv_mem_iff : ∀ {G : Type u_2} [inst : Group G] [inst_1 : StarMul G] (a b : G), a * b⁻¹ ∈ unitary G ↔ star a * a = star b * b
-- Mathlib.Topology.CompactOpen
ContinuousMap.isHomeomorph_coe : ∀ {X : Type u_2} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [DiscreteTopology X],
  IsHomeomorph DFunLike.coe
-- Mathlib.Tactic.Order.Graph.Basic
/-- Constructs a directed `Graph` using `≤` facts. It ignores all other facts.  -/
Mathlib.Tactic.Order.Graph.constructLeGraph : Array Mathlib.Tactic.Order.AtomicFact → Lean.MetaM Mathlib.Tactic.Order.Graph
-- Mathlib.Data.Nat.Cast.Basic
Nat.cast_pow : ∀ {α : Type u_1} [inst : Semiring α] (m n : ℕ), ↑(m ^ n) = ↑m ^ n